default search action
7th TACAS 2001: Genova, Italy (Part of ETAPS 2001)
- Tiziana Margaria, Wang Yi:
Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings. Lecture Notes in Computer Science 2031, Springer 2001, ISBN 3-540-41865-2
Invited Contributions
- Moshe Y. Vardi:
Branching vs. Linear Time: Final Showdown. 1-22 - Michael P. Fourman:
Propositional Reasoning. 23
Symbolic Verification
- Bernd Finkbeiner:
Language Containment Checking with Nondeterministic BDDs. 24-38 - Poul Frederick Williams, Henrik Reif Andersen, Henrik Hulgaard:
Satisfiability Checking Using Boolean Expression Diagrams. 39-51 - Tuba Yavuz-Kahveci, Murat Tuncer, Tevfik Bultan:
A Library for Composite Symbolic Representations. 52-66
Infinite State Systems: Deduction and Abstraction
- Michael Colón, Henny Sipma:
Synthesis of Linear Ranking Functions. 67-81 - Amir Pnueli, Sitvanit Ruah, Lenore D. Zuck:
Automatic Deductive Verification with Invisible Invariants. 82-97 - Yassine Lakhnech, Saddek Bensalem, Sergey Berezin, Sam Owre:
Incremental Verification by Abstraction. 98-112 - Ashish Tiwari, Harald Rueß, Hassen Saïdi, Natarajan Shankar:
A Technique for Invariant Generation. 113-127
Application of Model Checking Techniques
- Roberto Sebastiani, Alessandro Tomasi, Fausto Giunchiglia:
Model Checking Syllabi and Student Carreers. 128-142 - Xiang Fu
, Tevfik Bultan, Richard Hull, Jianwen Su:
Verification of Vortex Workflows. 143-157 - Thomas Ball, Sagar Chaki, Sriram K. Rajamani:
Parameterized Verification of Multithreaded Software Libraries. 158-173
Timed and Probabilistic Systems
- Gerd Behrmann, Ansgar Fehnker
Efficient Guiding Towards Cost-Optimality in UPPAAL. 174-188 - Thomas Hune, Judi Romijn, Mariëlle Stoelinga, Frits W. Vaandrager:
Linear Parametric Model Checking of Timed Automata. 189-203 - Suzana Andova, Jos C. M. Baeten:
Abstraction in Probabilistic Process Algebra. 204-219 - Theo C. Ruys, Rom Langerak
First Passage Time Analysis of Stochastic Process Algebra Using Partial Orders. 220-235
Hardware: Design and Verification
- Alan Mycroft, Richard Sharp:
Hardware/Software Co-Design Using Functional Languages. 236-251 - Miroslav N. Velev
Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors. 252-267
Software Verification
- Thomas Ball, Andreas Podelski, Sriram K. Rajamani:
Boolean and Cartesian Abstraction for Model Checking C Programs. 268-283 - Corina S. Pasareanu, Matthew B. Dwyer, Willem Visser:
Finding Feasible Counter-examples when Model Checking Abstracted Java Programs. 284-298 - Joachim van den Berg, Bart Jacobs:
The LOOP Compiler for Java and JML. 299-312
Symbolic Verification
- Alessandro Cimatti
Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking. 313-327 - Gianfranco Ciardo
Saturation: An Efficient Iteration Strategy for Symbolic State-Space Generation. 328-342
Testing: Techniques and Tools
- Brian Nielsen, Arne Skou
Automated Test Generation from Timed Automata. 343-357 - Sarfraz Khurshid:
Testing an Intentional Naming Scheme Using Genetic Algorithms. 358-372 - Filippo Ricca, Paolo Tonella
Building a Tool for the Analysis and Testing of Web Applications: Problems and Solutions. 373-388 - Amie L. Souter, Tiffany M. Wong, Stacey A. Shindo, Lori L. Pollock:
TATOO: Testing and Analysis Tool for Object- Oriented Software. 389-403
Implementation Techniques
- Marsha Chechik, Benet Devereux, Steve M. Easterbrook
Implementing a Multi-valued Symbolic Model Checker. 404-419 - Kathi Fisler
Is There a Best Symbolic Cycle-Detection Algorithm? 420-434 - Rubén Carvajal-Schiaffino, Giorgio Delzanno, Giovanni Chiola:
Combining Structural and Enumerative Techniques for the Validation of Bounded Petri Nets. 435-449 - Søren Christensen, Lars Michael Kristensen, Thomas Mailund:
A Sweep-Line Method for State Space Exploration. 450-464
Semantics and Compositional Verification
- Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler:
Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams. 465-479 - Li Tan, Rance Cleaveland:
Simulation Revisited. 480-495 - Elsa L. Gunter, Anca Muscholl, Doron A. Peled:
Compositional Message Sequence Charts. 496-511 - Jochen Klose, Hartmut Wittke:
An Automata Based Interpretation of Live Sequence Charts. 512-527
Logics and Model-Checking
- Hana Chockler, Orna Kupferman, Moshe Y. Vardi:
Coverage Metrics for Temporal Logic Model Checking. 528-542 - Benedikt Bollig, Martin Leucker
Parallel Model Checking for the Alternation Free µ-Calculus. 543-558 - Paritosh K. Pandya:
Model Checking CTL*[DC]. 559-573
ETAPS Tool Demonstration
- Michel Beaudouin-Lafon, Wendy E. Mackay, Mads Jensen, Peter Andersen, Paul Janecek, Henry Michael Lassen, Kasper Lund, Kjeld Høyer Mortensen, Stephanie Munck, Anne V. Ratzer, Katrine Ravn, Søren Christensen, Kurt Jensen:
CPN/Tools: A Tool for Editing and Simulating Coloured Petri Nets ETAPS Tool Demonstration Related to TACAS. 574-577 - Giuseppe Del Castillo
The ASM Workbench - A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models Tool Demonstration. 578-581 - Thomas Noll
The Erlang Verification Tool. 582-586
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-11-20 21:04 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: