| 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 |
図書
