Invited Contributions |
Branching vs. Linear Time: Final Showdown / M.Y. Vardi |
Propositional Reasoning / M.P. Fourman |
Symbolic Verification |
Language Containment Checking with Nondeterministic BDDs / B. Finkbeiner |
Satisfiability Checking Using Boolean Expression Diagrams / P.F. Williams ; H. Reif Andersen ; H. Hulgaard |
A Library for Composite Symbolic Representations / T. Yavuz-Kahveci ; M. Tuncer ; T. Bultan |
Infinite State Systems: Deduction and Abstraction |
Synthesis of Linear Ranking Functions / M.A. Colon ; H.B. Sipma |
Automatic Deductive Verification with Invisible Invariants / A. Pnueli ; S. Ruah ; L. Zuck |
Incremental Verification by Abstraction / Y. Lakhnech ; S. Bensalem ; S. Berezin ; S. Owre |
A Technique for Invariant Generation / A. Tiwari ; H. Rueβ ; H. Saïdi ; N. Shankar |
Application of Model Checking Techniques |
Model Checking Syllabi and Student Careers / R. Sebastiani ; A. Tomasi ; F. Giunchiglia |
Verification of Vortex Workflows / X. Fu ; R. Hull ; J. Su |
Parameterized Verification of Multithreaded Software Libraries / T. Ball ; S. Chaki ; S.K. Rajamani |
Timed and Probabilistic Systems |
Efficient Guiding Towards Cost-Optimality in UPPAAL / G. Behrmann ; A. Fehnker ; T. Hune ; K. Larsen ; P. Pettersson ; J. Romijn |
Linear Parametric Model Checking of Timed Automata / M. Stoelinga, ; F. Vaandrager |
Abstraction in Probabilistic Process Algebra / S. Andova ; J.CM. Baeten |
First Passage Time Analysis of Stochastic Process Algebra Using Partial Orders / T.C. Ruys ; R. Langerak ; J.-P. Katoen ; D. Latella ; M. Massik |
Hardware: Design and Verification |
Hardware/Software Co-design Using Functional Languages / A. Mycroft ; R. Sharp |
Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors / M.N. Velev |
Software Verification |
Boolean and Cartesian Abstraction for Model Checking C programs / A. Podelski |
Finding Feasible Counter-examples when Model Checking Abstracted Java Programs / C.S. Păs&abrebe;reanu ; M.B. Dwyer ; W. Visser |
The LOOP Compiler for Java and JML / J. van den Berg ; B. Jacobs |
Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking / A. Crmatti ; M. Roveri ; P. Bertoli |
Saturation: An Efficient Iteration Strategy for Symbolic State-Space Generation / G. Ciardo ; G. Lüttgen ; R. Siminiceanu |
Testing: Techniques and Tools |
Automated Test Generation from Timed Automata / B. Nielsen ; A. Skou |
Testing an Intentional Naming Scheme Using Genetic Algorithms / S. Khurshid |
Building a Tool for the Analysis and Testing of Web Applications: Problems and Solutions / F. Ricca ; P. Tonella |
TATOO: Testing and Analysis Tool for Object-Oriented Software / A.L. Souter ; T.M. Wong ; S.A. Shindo ; L.L. Pollock |
Implementation Techniques |
Implementing a Multi-valued Symbolic Model Checker / M. Chechik ; B. Devereux ; S. Easterbrook |
Is There a Best Symbolic Cycle-Detection Algorithm? / K. Fisler ; R. Fraer ; G. Kamhi ; M. Y. Vardi ; Z. Yang |
Combining Structural and Enumerative Techniques for the Validation of Bounded Petri Nets / R. Carvajal-Schiaffino ; G. Delzanno ; G. Chiola |
A Sweep-Line Method for State Space Exploration / S. Christensen ; L.M. Kristensen ; T. Mailund |
Semantics and Compositional Verification |
Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams / N. Amla ; E.A. Emerson ; K. Namjoshi ; R. Trefler |
Simulation Revisited / L. Tan ; R. Cleaveland |
Compositional Message Sequence Charts / E.L. Gunter ; A. Muscholl|CD.A. Peled |
An Automata Based Interpretation of Live Sequence Charts|CJ. Klose|CH. Wittke |
Logics and Model-Checking |
Coverage Metrics for Temporal Logic Model Checking|CH. Chockler|CO. Kupferman|CM. Y. Vardi |
Parallel Model Checking for the Alternation Free $$-Calculus|CB. Bollig / CM. Leucker ; M. Weber |
Model Checking CTL*[DC] / P.K. Pandya |
ETAPS Tool Demonstration |
CPN/Tools: A Tool for Editing and Simulating Coloured Petri Nets ETAPS Tool Demonstration Related to TACAS / M. Beaudomn-Lafon ; W.E. Mackay ; M. Jensen ; P. Andersen ; P. Janecek ; M. Lassen ; K. Lund ; K. Mortensen ; S. Munck ; A. Ratzer ; K. Ravn ; K. Jensen |
The ASM Workbench: A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models / G. Del Castillo |
The Erlang Verification Tool / T. Noll ; L. Fredlund ; D. Gurov |
Author Index |
Invited Contributions |
Branching vs. Linear Time: Final Showdown / M.Y. Vardi |
Propositional Reasoning / M.P. Fourman |