12. TACAS 2006: Vienna, Austria (Part of ETAPS 2006)

Holger Hermanns, Jens Palsberg (Eds.): Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006, Proceedings. Lecture Notes in Computer Science 3920 Springer 2006, ISBN 3-540-33056-9

Invited Contributions

Somesh Jha, Stefan Schwoon, Hao Wang, Thomas W. Reps:
Weighted Pushdown Systems and Trust-Management Systems. 1-26

Parametrization and Slicing

Jyotirmoy V. Deshmukh, E. Allen Emerson, Prateek Gupta:
Automatic Verification of Parameterized Data Structures. 27-41
Ping Yang, Samik Basu, C. R. Ramakrishnan:
Parameterized Verification of pi-Calculus Systems. 42-57
Geoffrey M. Brown, Lee Pike:
Easy Parameterized Verification of Biphase Mark and 8N1 Protocols. 58-72
Matthew B. Dwyer, John Hatcliff, Matthew Hoosier, Venkatesh Prasad Ranganath, Robby, Todd Wallentine:
Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs. 73-89

Symbolic Techniques

Radu Siminiceanu, Gianfranco Ciardo:
New Metrics for Static Variable Ordering in Decision Diagrams. 90-104
Neil Kettle, Andy King, Tadeusz Strzemecki:
Widening ROBDDs with Prime Implicants. 105-119
Dina Thomas, Supratik Chakraborty, Paritosh K. Pandya:
Efficient Guided Symbolic Reachability Using Reachability Expressions. 120-134

Satisfiability

Malay K. Ganai, Muralidhar Talupur, Aarti Gupta:
SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver. 135-150
Sagar Chaki:
SAT-Based Software Certification. 151-166
Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Fernanto Tiu:
Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants. 167-181
Hélène Collavizza, Michel Rueher:
Exploration of the Capabilities of Constraint Programming for Software Verification. 182-196

Abstraction

Barbara König, Vitali Kozioura:
Counterexample-Guided Abstraction Refinement for the Analysis of Graph Transformation Systems. 197-211
Arie Gurfinkel, Marsha Chechik:
Why Waste a Perfectly Good Abstraction?. 212-226
Bing Li, Fabio Somenzi:
Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking. 227-241
Daniel Kroening, Natasha Sharygina:
Approximating Predicate Images for Bit-Vector Logic. 242-256

Model Checking Algorithms

Krishnendu Chatterjee, Thomas A. Henzinger:
Finitary Winning in omega-Regular Games. 257-271
Peter Niebert, Doron Peled:
Efficient Model Checking for LTL with Partial Order Snapshots. 272-286
Dino Distefano, Peter W. O'Hearn, Hongseok Yang:
A Local Shape Analysis Based on Separation Logic. 287-302

Program Verification

Dan R. Ghica, Andrzej S. Murawski:
Compositional Model Extraction for Higher-Order Concurrent Programs. 303-317
Stefan Leue, Wei Wei:
A Region Graph Based Approach to Termination Proofs. 318-333
Sagar Chaki, Edmund M. Clarke, Nicholas Kidd, Thomas W. Reps, Tayssir Touili:
Verifying Concurrent Message-Passing C Programs with Recursive Calls. 334-349
Peter Habermehl, Radu Iosif, Tomás Vojnar:
Automata-Based Verification of Programs with Tree Updates. 350-364

Runtime Diagnostics

Atul Gupta, Pankaj Jalote:
An Experimental Comparison of the Effectiveness of Control Flow Based Testing Approaches on Seeded Faults. 365-378
Alex Groce, Rajeev Joshi:
Exploiting Traces in Program Analysis. 379-393

Quantitative Techniques

Koushik Sen, Mahesh Viswanathan, Gul Agha:
Model-Checking Markov Chains in the Presence of Uncertainties. 394-410
Joël Ouaknine, James Worrell:
Safety Metric Temporal Logic Is Fully Decidable. 411-425
Oleg Sokolsky, Sampath Kannan, Insup Lee:
Simulation-Based Graph Similarity. 426-440

Tool Demonstrations

Andrew Hinton, Marta Z. Kwiatkowska, Gethin Norman, David Parker:
PRISM: A Tool for Automatic Verification of Probabilistic Systems. 441-444
Hubert Garavel, Radu Mateescu, Damien Bergamini, Adrian Curic, Nicolas Descoubes, Christophe Joubert, Irina Smarandache-Sturm, Gilles Stragier:
DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation. 445-449
Alessio Lomuscio, Franco Raimondi:
MCMAS: A Model Checker for Multi-agent Systems. 450-454
Benedikt Bollig, Carsten Kern, Markus Schlütter, Volker Stolz:
MSCan - A Tool for Analyzing MSC Specifications. 455-458

Refinement

Ranjit Jhala, Kenneth L. McMillan:
A Practical and Complete Approach to Predicate Refinement. 459-473
Bhargav S. Gulavani, Sriram K. Rajamani:
Counterexample Driven Refinement for Abstract Interpretation. 474-488
Javier Esparza, Stefan Kiefer, Stefan Schwoon:
Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems. 489-503

Last update Sat May 18 19:51:04 2013 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page