TACAS 2004

43 papers

1. A Class of Polynomially Solvable Range Constraints for Interval Analysis without Widenings and Narrowings · Zhendong Su, David A. Wagner
2. A Partial Order Semantics Approach to the Clock Explosion Problem of Timed Automata · Denis Lugiez, Peter Niebert, Sarah Zennou
3. A Scalable Incomplete Test for the Boundedness of UML RT Models · Stefan Leue, Richard Mayr, Wei Wei
4. A Temporal Logic of Nested Calls and Returns · Rajeev Alur, Kousha Etessami, P. Madhusudan
5. A Tool for Checking ANSI-C Programs · Edmund M. Clarke, Daniel Kroening, Flavio Lerda
6. An Interpolating Theorem Prover · Kenneth L. McMillan
7. Applying Game Semantics to Compositional Software Modeling and Verification · Samson Abramsky, Dan R. Ghica, Andrzej S. Murawski, C.-H. Luke Ong
8. Automated Generation of a Progress Measure for the Sweep-Line Method · Karsten Schmidt
9. Automatic Creation of Environment Models via Training · Thomas Ball, Vladimir Levin, Fei Xie
10. Automatic Parametric Verification of a Root Contention Protocol Based on Abstract State Machines and First Order Timed Logic · Danièle Beauquier, Tristan Crolard, Evguenia Prokofieva
11. Automatic Verification of Time Sensitive Cryptographic Protocols · Giorgio Delzanno, Pierre Ganty
12. Binding-Time Analysis for MetaML via Type Inference and Constraint Solving · Nathan Linger, Tim Sheard
13. Checking Strong Specifications Using an Extensible Software Model Checking Framework · Robby, Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff
14. CoPS - Checker of Persistent Security · Carla Piazza, Enrico Pivato, Sabina Rossi
15. Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata · Pavel Krcál, Wang Yi
16. Efficient Computation of Time-Bounded Reachability Probabilities in Uniform Continuous-Time Markov Decision Processes · Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen
17. Error Explanation with Distance Metrics · Alex Groce
18. FASTer Acceleration of Counter Automata in Practice · Sébastien Bardin, Alain Finkel, Jérôme Leroux
19. From Complementation to Certification · Orna Kupferman, Moshe Y. Vardi
20. Guided Invariant Model Checking Based on Abstraction and Symbolic Pattern Databases · Kairong Qian, Albert Nymeyer
21. How Vacuous Is Vacuous? · Arie Gurfinkel, Marsha Chechik
22. Liveness with Incomprehensible Ranking · Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck
23. Lower and Upper Bounds in Zone Based Abstractions of Timed Automata · Gerd Behrmann, Patricia Bouyer, Kim Guldstrand Larsen, Radek Pelánek
24. MetaGame: An Animation Tool for Model-Checking Games · Markus Müller-Olm, Haiseung Yoo
25. Minimal Assignments for Bounded Model Checking · Kavita Ravi, Fabio Somenzi
26. Model Checking Discounted Temporal Properties · Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Mariëlle Stoelinga
27. Monotonic Abstraction-Refinement for CTL · Sharon Shoham, Orna Grumberg
28. Numeric Domains with Summarized Dimensions · Denis Gopan, Frank DiMaio, Nurit Dor, Thomas W. Reps, Shmuel Sagiv
29. Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study · Håkan L. S. Younes, Marta Z. Kwiatkowska, Gethin Norman, David Parker
30. Obtaining Memory-Efficient Reachability Graph Representations Using the Sweep-Line Method · Thomas Mailund, Michael Westergaard
31. Omega-Regular Model Checking · Bernard Boigelot, Axel Legay, Pierre Wolper
32. Online Efficient Predictive Safety Analysis of Multithreaded Programs · Koushik Sen, Grigore Rosu, Gul Agha
33. Refining Approximations in Software Predicate Abstraction · Thomas Ball, Byron Cook, Satyaki Das, Sriram K. Rajamani
34. Resource-Optimal Scheduling Using Priced Timed Automata · Jacob Illum Rasmussen, Kim Guldstrand Larsen, K. Subramani
35. Revisiting Positive Equality · Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur
36. Simulation-Based Verification of Autonomous Controllers via Livingstone PathFinder · A. E. Lindsey, Charles Pecheur
37. Solving Disjunctive/Conjunctive Boolean Equation Systems with Alternating Fixed Points · Jan Friso Groote, Misa Keinänen
38. Symbolically Computing Most-Precise Abstract Operations for Shape Analysis · Greta Yorsh, Thomas W. Reps, Shmuel Sagiv
39. SyncGen: An Aspect-Oriented Framework for Synchronization · Xianghua Deng, Matthew B. Dwyer, John Hatcliff, Masaaki Mizuno
40. Tampere Verification Tool · Heikki Virtanen, Henri Hansen, Antti Valmari, Juha Nieminen, Timo Erkkilä
41. Tarjan's Algorithm Makes On-the-Fly LTL Verification More Efficient · Jaco Geldenhuys, Antti Valmari
42. The Succinct Solver Suite · Flemming Nielson, Hanne Riis Nielson, Hongyan Sun, Mikael Buchholtz, René Rydhof Hansen, Henrik Pilegaard + 1 more
43. Vooduu: Verification of Object-Oriented Designs Using UPPAAL · Karsten Diethers, Michaela Huhn