TACAS 2006

35 papers

1. A Local Shape Analysis Based on Separation Logic · Dino Distefano, Peter W. O'Hearn, Hongseok Yang
2. A Practical and Complete Approach to Predicate Refinement · Ranjit Jhala, Kenneth L. McMillan
3. A Region Graph Based Approach to Termination Proofs · Stefan Leue, Wei Wei
4. Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems · Javier Esparza, Stefan Kiefer, Stefan Schwoon
5. An Experimental Comparison of the Effectiveness of Control Flow Based Testing Approaches on Seeded Faults · Atul Gupta, Pankaj Jalote
6. Approximating Predicate Images for Bit-Vector Logic · Daniel Kroening, Natasha Sharygina
7. Automata-Based Verification of Programs with Tree Updates · Peter Habermehl, Radu Iosif, Tomás Vojnar
8. Automatic Verification of Parameterized Data Structures · Jyotirmoy V. Deshmukh, E. Allen Emerson, Prateek Gupta
9. Compositional Model Extraction for Higher-Order Concurrent Programs · Dan R. Ghica, Andrzej S. Murawski
10. Counterexample Driven Refinement for Abstract Interpretation · Bhargav S. Gulavani, Sriram K. Rajamani
11. Counterexample-Guided Abstraction Refinement for the Analysis of Graph Transformation Systems · Barbara König, Vitali Kozioura
12. DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation · Hubert Garavel, Radu Mateescu, Damien Bergamini, Adrian Curic, Nicolas Descoubes, Christophe Joubert + 2 more
13. Easy Parameterized Verification of Biphase Mark and 8N1 Protocols · Geoffrey M. Brown, Lee Pike
14. Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking · Bing Li, Fabio Somenzi
15. Efficient Guided Symbolic Reachability Using Reachability Expressions · Dina Thomas, Supratik Chakraborty, Paritosh K. Pandya
16. Efficient Model Checking for LTL with Partial Order Snapshots · Peter Niebert, Doron A. Peled
17. Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs · Matthew B. Dwyer, John Hatcliff, Matthew Hoosier, Venkatesh Prasad Ranganath, Robby, Todd Wallentine
18. Exploiting Traces in Program Analysis · Alex Groce, Rajeev Joshi
19. Exploration of the Capabilities of Constraint Programming for Software Verification · Hélène Collavizza, Michel Rueher
20. Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants · Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Fernanto Tiu
21. Finitary Winning in omega-Regular Games · Krishnendu Chatterjee, Thomas A. Henzinger
22. MCMAS: A Model Checker for Multi-agent Systems · Alessio Lomuscio, Franco Raimondi
23. MSCan - A Tool for Analyzing MSC Specifications · Benedikt Bollig, Carsten Kern, Markus Schlütter, Volker Stolz
24. Model-Checking Markov Chains in the Presence of Uncertainties · Koushik Sen, Mahesh Viswanathan, Gul Agha
25. New Metrics for Static Variable Ordering in Decision Diagrams · Radu Siminiceanu, Gianfranco Ciardo
26. PRISM: A Tool for Automatic Verification of Probabilistic Systems · Andrew Hinton, Marta Z. Kwiatkowska, Gethin Norman, David Parker
27. Parameterized Verification of pi-Calculus Systems · Ping Yang, Samik Basu, C. R. Ramakrishnan
28. SAT-Based Software Certification · Sagar Chaki
29. SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver · Malay K. Ganai, Muralidhar Talupur, Aarti Gupta
30. Safety Metric Temporal Logic Is Fully Decidable · Joël Ouaknine, James Worrell
31. Simulation-Based Graph Similarity · Oleg Sokolsky, Sampath Kannan, Insup Lee
32. Verifying Concurrent Message-Passing C Programs with Recursive Calls · Sagar Chaki, Edmund M. Clarke, Nicholas Kidd, Thomas W. Reps, Tayssir Touili
33. Weighted Pushdown Systems and Trust-Management Systems · Somesh Jha, Stefan Schwoon, Hao Wang, Thomas W. Reps
34. Why Waste a Perfectly Good Abstraction? · Arie Gurfinkel, Marsha Chechik
35. Widening ROBDDs with Prime Implicants · Neil Kettle, Andy King, Tadeusz Strzemecki