7. TACAS 2001: Genova, Italy (Part of ETAPS 2001)

@proceedings{DBLP:conf/tacas/2001,
  editor    = {Tiziana Margaria and
               Wang Yi},
  title     = {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},
  booktitle = {TACAS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2031},
  year      = {2001},
  isbn      = {3-540-41865-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

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, Joost-Pieter Katoen, Diego Latella, Mieke Massink:
  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, Marco Roveri, Piergiorgio Bertoli:
  Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking. 313-327
  
• Gianfranco Ciardo, Gerald Lüttgen, Radu Siminiceanu:
  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, Ranan Fraer, Gila Kamhi, Moshe Y. Vardi, Zijiang Yang:
  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 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, Michael Weber:
  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, Lars-Åke Fredlund, Dilian Gurov:
  The Erlang Verification Tool. 582-586