CAV 2005

52 papers

1. A Policy Iteration Algorithm for Computing Fixed Points in Static Analysis of Programs · Alexandru Costan, Stephane Gaubert, Eric Goubault, Matthieu Martel, Sylvie Putot
2. Abstraction Refinement for Bounded Model Checking · Anubhav Gupta, Ofer Strichman
3. Abstraction Refinement via Inductive Learning · Alexey Loginov, Thomas W. Reps, Shmuel Sagiv
4. Abstraction for Falsification · Thomas Ball, Orna Kupferman, Greta Yorsh
5. Action Language Verifier, Extended · Tuba Yavuz-Kahveci, Constantinos Bartzis, Tevfik Bultan
6. Algorithmic Algebraic Model Checking I: Challenges from Systems Biology · Carla Piazza, Marco Antoniotti, Venkatesh Mysore, Alberto Policriti, Franz Winkler, Bud Mishra
7. Automated Assume-Guarantee Reasoning for Simulation Conformance · Sagar Chaki, Edmund M. Clarke, Nishant Sinha, Prasanna Thati
8. Bounded Model Checking of Concurrent Programs · Ishai Rabinovitz, Orna Grumberg
9. Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework · Matthew B. Dwyer, John Hatcliff, Matthew Hoosier, Robby
10. Cogent: Accurate Theorem Proving for Program Verification · Byron Cook, Daniel Kroening, Natasha Sharygina
11. Compositional Analysis of Floating-Point Linear Numerical Filters · David Monniaux
12. Concrete Model Checking with Abstract Matching and Refinement · Corina S. Pasareanu, Radek Pelánek, Willem Visser
13. DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic · Robert Nieuwenhuis, Albert Oliveras
14. Data Structure Specifications via Local Equality Axioms · Scott McPeak, George C. Necula
15. Efficient Monitoring of omega-Languages · Marcelo d'Amorim, Grigore Rosu
16. Efficient Satisfiability Modulo Theories via Delayed Theory Combination · Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum + 1 more
17. Expand, Enlarge and Check... Made Efficient · Gilles Geeraerts, Jean-François Raskin, Laurent Van Begin
18. Extended Weighted Pushdown Systems · Akash Lal, Thomas W. Reps, Gogul Balakrishnan
19. F-Soft: Software Verification Platform · Franjo Ivancic, Zijiang Yang, Malay K. Ganai, Aarti Gupta, Ilya Shlyakhter, Pranav Ashar
20. Formal Verification of Backward Compatibility of Microcode · Tamarah Arons, Elad Elster, Limor Fix, Sela Mador-Haim, Michael Mishaeli, Jonathan Shalev + 4 more
21. Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive Invariants · Roope Kaivola
22. IIV: An Invisible Invariant Verifier · Ittai Balaban, Yi Fang, Amir Pnueli, Lenore D. Zuck
23. Improved Probabilistic Models for 802.11 Protocol Verification · Amitabha Roy, K. Gopinath
24. Incremental Algorithms for Inter-procedural Analysis of Safety Properties · Christopher L. Conway, Kedar S. Namjoshi, Dennis Dams, Stephen A. Edwards
25. Incremental and Complete Bounded Model Checking for Full PLTL · Keijo Heljanko, Tommi A. Junttila, Timo Latvala
26. Interpolant-Based Transition Relation Approximation · Ranjit Jhala, Kenneth L. McMillan
27. JVer: A Java Verifier · Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee, George C. Necula
28. Linear Ranking with Reachability · Aaron R. Bradley, Zohar Manna, Henny B. Sipma
29. Model Checking x86 Executables with CodeSurfer/x86 and WPDS++ · Gogul Balakrishnan, Thomas W. Reps, Nicholas Kidd, Akash Lal, Junghee Lim, David Melski + 4 more
30. On Statistical Model Checking of Stochastic Systems · Koushik Sen, Mahesh Viswanathan, Gul Agha
31. Predicate Abstraction via Symbolic Decision Procedures · Shuvendu K. Lahiri, Thomas Ball, Byron Cook
32. Probabilistic Verification for "Black-Box" Systems · Håkan L. S. Younes
33. Program Repair as a Game · Barbara Jobstmann, Andreas Griesmayer, Roderick Bloem
34. Randomized Algorithms for Program Analysis and Verification · George C. Necula, Sumit Gulwani
35. Reasoning About Threads Communicating via Locks · Vineet Kahlon, Franjo Ivancic, Aarti Gupta
36. Romeo: A Tool for Analyzing Time Petri Nets · Guillaume Gardey, Didier Lime, Morgan Magnin, Olivier H. Roux
37. SMT-COMP: Satisfiability Modulo Theories Competition · Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump
38. Saturn: A SAT-Based Tool for Bug Detection · Yichen Xie, Alex Aiken
39. Symbolic Compositional Verification by Learning Assumptions · Rajeev Alur, P. Madhusudan, Wonhong Nam
40. Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking · Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi
41. Symmetry Reduction in SAT-Based Model Checking · Daijue Tang, Sharad Malik, Aarti Gupta, C. Norris Ip
42. Syntax-Driven Reachable State Space Construction of Synchronous Reactive Programs · Eric Vecchié, Robert de Simone
43. TRANSYT: A Tool for the Verification of Asynchronous Concurrent Systems · Enric Pastor, Marco A. Peña, Marc Solé
44. TVOC: A Translation Validator for Optimizing Compilers · Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, Lenore D. Zuck
45. The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications · Alessandro Armando, David A. Basin, Yohan Boichut, Yannick Chevalier, Luca Compagna, Jorge Cuéllar + 11 more
46. The ComFoRT Reasoning Framework · Sagar Chaki, James Ivers, Natasha Sharygina, Kurt C. Wallnau
47. The Orchids Intrusion Detection Tool · Julien Olivain, Jean Goubault-Larrecq
48. Validating a Modern Microprocessor · Bob Bentley
49. Verification of Tree Updates for Optimization · Michael Benedikt, Angela Bonifati, Sergio Flesca, Avinash Vyas
50. Wolf - Bug Hunter for Concurrent Software Using Formal Methods · Sharon Barner, Ziv Glazberg, Ishai Rabinovitz
51. Yet Another Decision Procedure for Equality Logic · Orly Meir, Ofer Strichman
52. Ymer: A Statistical Model Checker · Håkan L. S. Younes