CAV 2004

51 papers

1. A Formal Reduction for Lock-Free Parallel Algorithms · Hui Gao, Wim H. Hesselink
2. A Toolset for Modelling and Verification of GALS Systems · S. Ramesh, Sampada Sonalkar, Vijay D'Silva, Naveen Chandra, B. Vijayalakshmi
3. Abstract Regular Model Checking · Ahmed Bouajjani, Peter Habermehl, Tomás Vojnar
4. Abstraction-Based Satisfiability Solving of Presburger Arithmetic · Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman
5. An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking · Kedar S. Namjoshi
6. An Experimental Evaluation of Ground Decision Procedures · Leonardo Mendonça de Moura, Harald Rueß
7. Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values · Jesse D. Bingham, Anne Condon, Alan J. Hu, Shaz Qadeer, Zhichuan Zhang
8. CVC Lite: A New Implementation of the Cooperating Validity Checker Category B · Clark W. Barrett, Sergey Berezin
9. CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking · HoonSang Jin, Mohammad Awedh, Fabio Somenzi
10. Compositional Specification and Model Checking in GSTE · Jin Yang, Carl-Johan H. Seger
11. DPLL( T): Fast Decision Procedures · Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
12. Deductive Verification of Pipelined Machines Using First-Order Quantification · Sandip Ray, Warren A. Hunt Jr.
13. Efficient Modeling of Embedded Memories in Bounded Model Checking · Malay K. Ganai, Aarti Gupta, Pranav Ashar
14. Formal Analysis of Java Programs in JavaFAN · Azadeh Farzan, Feng Chen, José Meseguer, Grigore Rosu
15. Functional Dependency for Verification Reduction · Jie-Hong Roland Jiang, Robert K. Brayton
16. GSTE Is Partitioned Model Checking · Roberto Sebastiani, Eli Singerman, Stefano Tonetta, Moshe Y. Vardi
17. Global Model-Checking of Infinite-State Systems · Nir Piterman, Moshe Y. Vardi
18. Image Computation in Infinite State Model Checking · Alain Finkel, Jérôme Leroux
19. Indexed Predicate Discovery for Unbounded System Verification · Shuvendu K. Lahiri, Randal E. Bryant
20. JNuke: Efficient Dynamic Analysis for Java · Cyrille Artho, Viktor Schuppan, Armin Biere, Pascal Eugster, Marcel Baur, Boris Zweimüller
21. MCK: Model Checking the Logic of Knowledge · Peter Gammie, Ron van der Meyden
22. Mechanical Mathematical Methods for Microprocessor Verification · Warren A. Hunt Jr.
23. ObsSlice: A Timed Automata Slicer Based on Observers · Víctor A. Braberman, Diego Garbervetsky, Alfredo Olivero
24. Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings · Claus Schröter, Victor Khomenko
25. PlayGame: A Platform for Diagnostic Games · Li Tan
26. Proving More Properties with Bounded Model Checking · Mohammad Awedh, Fabio Somenzi
27. QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings · Ganesh Gopalakrishnan, Yue Yang, Hemanthkumar Sivaraj
28. Range Allocation for Separation Logic · Muralidhar Talupur, Nishant Sinha, Ofer Strichman, Amir Pnueli
29. Regular Model Checking for LTL(MSO) · Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, Julien d'Orso, Mayank Saksena
30. Rob Tristan Gerth: 1956?2003 · John O'Leary, Marly Roncken
31. SAL 2 · Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar, Maria Sorea + 1 more
32. Static Program Analysis via 3-Valued Logic · Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm
33. Statistical Model Checking of Black-Box Probabilistic Systems · Koushik Sen, Mahesh Viswanathan, Gul Agha
34. Stuck-Free Conformance · Cédric Fournet, C. A. R. Hoare, Sriram K. Rajamani, Jakob Rehof
35. Symbolic Model Checking of Non-regular Properties · Martin Lange
36. Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures · Farn Wang
37. Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors · Amit Goel, Randal E. Bryant
38. Termination of Linear Programs · Ashish Tiwari
39. The HiVy Tool Set · Paula J. Pingree, Erich Mikk
40. The Mec 5 Model-Checker · Alain Griffault, Aymeric Vincent
41. The UCLID Decision Procedure · Shuvendu K. Lahiri, Sanjit A. Seshia
42. Understanding Counterexamples with explain · Alex Groce, Daniel Kroening, Flavio Lerda
43. Using Interface Refinement to Integrate Formal Verification into the Design Cycle · Jacob Chang, Sergey Berezin, David L. Dill
44. Verification of an Advanced mips-Type Out-of-Order Execution Algorithm · Tamarah Arons
45. Verification via Structure Simulation · Neil Immerman, Alexander Moshe Rabinovich, Thomas W. Reps, Shmuel Sagiv, Greta Yorsh
46. Verifying omega-Regular Properties of Markov Chains · Doron Bustan, Sasha Rubin, Moshe Y. Vardi
47. WSAT: A Tool for Formal Analysis of Web Services · Xiang Fu, Tevfik Bultan, Jianwen Su
48. Why Model Checking Can Improve WCET Analysis · Alexander Metzner
49. Widening Arithmetic Automata · Constantinos Bartzis, Tevfik Bultan
50. Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement · Thomas Ball, Byron Cook, Shuvendu K. Lahiri, Lintao Zhang
51. Zing: A Model Checker for Concurrent Software · Tony Andrews, Shaz Qadeer, Sriram K. Rajamani, Jakob Rehof, Yichen Xie