| 2001 | A Library for Composite Symbolic Representations. Tuba Yavuz-Kahveci, Murat Tuncer, Tevfik Bultan |
| 2001 | A Sweep-Line Method for State Space Exploration. Søren Christensen, Lars Michael Kristensen, Thomas Mailund |
| 2001 | A Technique for Invariant Generation. Ashish Tiwari, Harald Rueß, Hassen Saïdi, Natarajan Shankar |
| 2001 | Abstraction in Probabilistic Process Algebra. Suzana Andova, Jos C. M. Baeten |
| 2001 | An Automata Based Interpretation of Live Sequence Charts. Jochen Klose, Hartmut Wittke |
| 2001 | Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams. Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler |
| 2001 | Automated Test Generation from Timed Automata. Brian Nielsen, Arne Skou |
| 2001 | Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors. Miroslav N. Velev |
| 2001 | Automatic Deductive Verification with Invisible Invariants. Amir Pnueli, Sitvanit Ruah, Lenore D. Zuck |
| 2001 | Boolean and Cartesian Abstraction for Model Checking C Programs. Thomas Ball, Andreas Podelski, Sriram K. Rajamani |
| 2001 | Branching vs. Linear Time: Final Showdown. Moshe Y. Vardi |
| 2001 | Building a Tool for the Analysis and Testing of Web Applications: Problems and Solutions. Filippo Ricca, Paolo Tonella |
| 2001 | CPN/Tools: A Tool for Editing and Simulating Coloured Petri Nets ETAPS Tool Demonstration Related to TACAS. 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 |
| 2001 | Combining Structural and Enumerative Techniques for the Validation of Bounded Petri Nets. Rubén Carvajal-Schiaffino, Giorgio Delzanno, Giovanni Chiola |
| 2001 | Compositional Message Sequence Charts. Elsa L. Gunter, Anca Muscholl, Doron A. Peled |
| 2001 | Coverage Metrics for Temporal Logic Model Checking. Hana Chockler, Orna Kupferman, Moshe Y. Vardi |
| 2001 | Efficient Guiding Towards Cost-Optimality in UPPAAL. Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim G. Larsen, Paul Pettersson, Judi Romijn |
| 2001 | Finding Feasible Counter-examples when Model Checking Abstracted Java Programs. Corina S. Pasareanu, Matthew B. Dwyer, Willem Visser |
| 2001 | First Passage Time Analysis of Stochastic Process Algebra Using Partial Orders. Theo C. Ruys, Rom Langerak, Joost-Pieter Katoen, Diego Latella, Mieke Massink |
| 2001 | Hardware/Software Co-Design Using Functional Languages. Alan Mycroft, Richard Sharp |
| 2001 | Implementing a Multi-valued Symbolic Model Checker. Marsha Chechik, Benet Devereux, Steve M. Easterbrook |
| 2001 | Incremental Verification by Abstraction. Yassine Lakhnech, Saddek Bensalem, Sergey Berezin, Sam Owre |
| 2001 | Is There a Best Symbolic Cycle-Detection Algorithm? Kathi Fisler, Ranan Fraer, Gila Kamhi, Moshe Y. Vardi, Zijiang Yang |
| 2001 | Language Containment Checking with Nondeterministic BDDs. Bernd Finkbeiner |
| 2001 | Linear Parametric Model Checking of Timed Automata. Thomas Hune, Judi Romijn, Mariëlle Stoelinga, Frits W. Vaandrager |
| 2001 | Model Checking CTL*[DC]. Paritosh K. Pandya |
| 2001 | Model Checking Syllabi and Student Carreers. Roberto Sebastiani, Alessandro Tomasi, Fausto Giunchiglia |
| 2001 | Parallel Model Checking for the Alternation Free µ-Calculus. Benedikt Bollig, Martin Leucker, Michael Weber |
| 2001 | Parameterized Verification of Multithreaded Software Libraries. Thomas Ball, Sagar Chaki, Sriram K. Rajamani |
| 2001 | Propositional Reasoning. Michael P. Fourman |
| 2001 | Satisfiability Checking Using Boolean Expression Diagrams. Poul Frederick Williams, Henrik Reif Andersen, Henrik Hulgaard |
| 2001 | Saturation: An Efficient Iteration Strategy for Symbolic State-Space Generation. Gianfranco Ciardo, Gerald Lüttgen, Radu Siminiceanu |
| 2001 | Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking. Alessandro Cimatti, Marco Roveri, Piergiorgio Bertoli |
| 2001 | Simulation Revisited. Li Tan, Rance Cleaveland |
| 2001 | Synthesis of Linear Ranking Functions. Michael Colón, Henny Sipma |
| 2001 | TATOO: Testing and Analysis Tool for Object- Oriented Software. Amie L. Souter, Tiffany M. Wong, Stacey A. Shindo, Lori L. Pollock |
| 2001 | Testing an Intentional Naming Scheme Using Genetic Algorithms. Sarfraz Khurshid |
| 2001 | The ASM Workbench - A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models Tool Demonstration. Giuseppe Del Castillo |
| 2001 | The Erlang Verification Tool. Thomas Noll, Lars-Åke Fredlund, Dilian Gurov |
| 2001 | The LOOP Compiler for Java and JML. Joachim van den Berg, Bart Jacobs |
| 2001 | 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 Tiziana Margaria, Wang Yi |
| 2001 | Verification of Vortex Workflows. Xiang Fu, Tevfik Bultan, Richard Hull, Jianwen Su |