default search action
9th TACAS 2003: Warsaw, Poland (Part of ETAPS 2003)
- Hubert Garavel, John Hatcliff:
Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings. Lecture Notes in Computer Science 2619, Springer 2003, ISBN 3-540-00898-5
Invited Contributions
- Peter Lee:
What Are We Trying to Prove? Reflections on Experiences with Proof-Carrying Code. 1
Bounded Model Checking and SAT-Based Methods
- Kenneth L. McMillan, Nina Amla:
Automatic Abstraction without Counterexamples. 2-17 - Marco Benedetti, Alessandro Cimatti
:
Bounded Model Checking for Past LTL. 18-33 - Nina Amla, Robert P. Kurshan, Kenneth L. McMillan, Ricardo H. Medel
Experimental Analysis of Different Techniques for Bounded Model Checking. 34-48
Mu-Calculus and Temporal Logics
- Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar:
On the Universal and Existential Fragments of the µ-Calculus. 49-64 - Roy Armoni, Doron Bustan, Orna Kupferman, Moshe Y. Vardi:
Resets vs. Aborts in Linear Temporal Logic. 65-80 - Radu Mateescu:
A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems. 81-96
Verification of Parameterized Systems
- Pascal Fontaine, E. Pascal Gribomont:
Decidability of Invariant Validation for Paramaterized Systems. 97-112 - Dmitri Chkliaev, Jozef Hooman, Erik P. de Vink:
Verification and Improvement of the Sliding Window Protocol. 113-127 - Javier Esparza
Simple Representative Instantiations for Multicast Protocols. 128-143 - E. Allen Emerson, Vineet Kahlon:
Rapid Parameterized Model Checking of Snoopy Cache Coherence Protocols. 144-159
Abstractions and Counter-Examples
- Arie Gurfinkel
Proof-Like Counter-Examples. 160-175 - Marcelo Glusman, Gila Kamhi, Sela Mador-Haim, Ranan Fraer, Moshe Y. Vardi:
Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation. 176-191 - Edmund M. Clarke, Ansgar Fehnker
Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement. 192-207 - Rajeev Alur, Thao Dang, Franjo Ivancic:
Counter-Example Guided Predicate Abstraction of Hybrid Systems. 208-223
Real-Time and Scheduling
- Elena Fersman, Leonid Mokrushin, Paul Pettersson
Schedulability Analysis Using Two Clocks. 224-239 - Yasmina Abdeddaïm, Eugene Asarin
On Optimal Scheduling under Uncertainty. 240-253 - Gerd Behrmann, Patricia Bouyer, Emmanuel Fleury, Kim Guldstrand Larsen:
Static Guard Analysis in Timed Automata Verification. 254-277 - Piotr Dembinski, Agata Janowska, Pawel Janowski, Wojciech Penczek, Agata Pólrola
Verics: A Tool for Verifying Timed Automata and Estelle Specifications. 278-283
Security and Cryptography
- Ivan Cibrario Bertolotti, Luca Durante
A New Knowledge Representation Strategy for Cryptographic Protocol Analysis. 284-298 - Liana Bozga, Yassine Lakhnech, Michaël Périn:
Pattern-Based Abstraction for Verifying Secrecy in Protocols. 299-314
Modules and Compositional Verification
- Samik Basu, C. R. Ramakrishnan:
Compositional Analysis for Verification of Parameterized Systems. 315-330 - Jamieson M. Cobleigh, Dimitra Giannakopoulou, Corina S. Pasareanu:
Learning Assumptions for Compositional Verification. 331-346 - Stavros Tripakis:
Automated Module Composition. 347-362 - Rajeev Alur, Salvatore La Torre, P. Madhusudan:
Modular Strategies for Recursive Game Graphs. 363-378
Symbolic State Spaces and Decision Diagrams
- Gianfranco Ciardo
Saturation Unbound. 379-393 - Constantinos Bartzis, Tevfik Bultan:
Construction of Efficient BDDs for Bounded Arithmetic Constraints. 394-408
Performance and Mobility
- Oleg Sokolsky, Anna Philippou, Insup Lee, Kyriakos Christou:
Modeling and Analysis of Power-Aware Systems. 409-425 - Holger Hermanns, Christophe Joubert
A Set of Performance and Dependability Analysis Components for CADP. 425-430 - Dezhuang Zhang, Rance Cleaveland, Eugene W. Stark:
The Integrated CWB-NC/PIOATool for Functional Verification and Performance Analysis of Concurrent Systems. 431-436 - Chiara Braghin, Agostino Cortesi
BANANA - A Tool for Boundary Ambients Nesting ANAlysis. 437-441
State Space Reductions
- Bernard Berthomieu, François Vernadat:
State Class Constructions for Branching Analysis of Time Petri Nets. 442-457 - Victor Khomenko, Maciej Koutny:
Branching Processes of High-Level Petri Nets. 458-472 - Karsten Schmidt:
Using Petri Net Invariants in State Space Construction. 473-488 - Scott D. Stoller, Ernie Cohen:
Optimistic Synchronization-Based State-Space Reduction. 489-504
Constraint-Solving and Decision Procedures
- Mandana Vaziri, Daniel Jackson:
Checking Properties of Heap-Manipulating Procedures with a Constraint Solver. 505-520 - Sergey Berezin, Vijay Ganesh
An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic. 521-536 - Sylvain Conchon, Sava Krstic:
Strategies for Combining Decision Procedures. 537-552
Testing and Verification
- Sarfraz Khurshid, Corina S. Pasareanu, Willem Visser:
Generalized Symbolic Execution for Model Checking and Testing. 553-568 - Fabrice Baray, Philippe Codognet, Daniel Diaz
Code-Based Test Generation for Validation of Functional Processor Descriptions. 569-584 - Jan Friso Groote
Large State Space Visualization. 585-590 - Céline Bigot, Alain Faivre, Jean-Pierre Gallois, Arnault Lapitre, David Lugato, Jean-Yves Pierron, Nicolas Rapin:
Automatic Test Generation with AGATHA. 591-596 - Sebastián Uchitel, Robert Chatley, Jeff Kramer, Jeff Magee:
LTSA-MSC: Tool Support for Behaviour Model Elaboration Using Implied Scenarios. 597-601
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-04 20:30 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: