default search action
10th TACAS 2004: Barcelona, Spain (Part of ETAPS 2004)
- Kurt Jensen, Andreas Podelski:
Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings. Lecture Notes in Computer Science 2988, Springer 2004, ISBN 3-540-21299-X
Theorem Proving
- Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur:
Revisiting Positive Equality. 1-15 - Kenneth L. McMillan:
An Interpolating Theorem Prover. 16-30 - Kavita Ravi, Fabio Somenzi:
Minimal Assignments for Bounded Model Checking. 31-45
Probabilistic Model Checking
- Håkan L. S. Younes, Marta Z. Kwiatkowska, Gethin Norman, David Parker
:
Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study. 46-60 - Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen:
Efficient Computation of Time-Bounded Reachability Probabilities in Uniform Continuous-Time Markov Decision Processes. 61-76 - Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Mariëlle Stoelinga:
Model Checking Discounted Temporal Properties. 77-92
Testing
- Thomas Ball, Vladimir Levin, Fei Xie:
Automatic Creation of Environment Models via Training. 93-107 - Alex Groce:
Error Explanation with Distance Metrics. 108-122 - Koushik Sen, Grigore Rosu, Gul Agha:
Online Efficient Predictive Safety Analysis of Multithreaded Programs. 123-138
Tools
- Karsten Diethers, Michaela Huhn:
Vooduu: Verification of Object-Oriented Designs Using UPPAAL. 139-143 - Carla Piazza, Enrico Pivato, Sabina Rossi:
CoPS - Checker of Persistent Security. 144-152 - Heikki Virtanen, Henri Hansen, Antti Valmari, Juha Nieminen, Timo Erkkilä:
Tampere Verification Tool. 153-157 - Xianghua Deng, Matthew B. Dwyer, John Hatcliff, Masaaki Mizuno:
SyncGen: An Aspect-Oriented Framework for Synchronization. 158-162 - Markus Müller-Olm, Haiseung Yoo:
MetaGame: An Animation Tool for Model-Checking Games. 163-167 - Edmund M. Clarke, Daniel Kroening, Flavio Lerda:
A Tool for Checking ANSI-C Programs. 168-176
Explicite State / Petri Nets
- Thomas Mailund, Michael Westergaard:
Obtaining Memory-Efficient Reachability Graph Representations Using the Sweep-Line Method. 177-191 - Karsten Schmidt:
Automated Generation of a Progress Measure for the Sweep-Line Method. 192-204 - Jaco Geldenhuys, Antti Valmari:
Tarjan's Algorithm Makes On-the-Fly LTL Verification More Efficient. 205-219
Scheduling
- Jacob Illum Rasmussen, Kim Guldstrand Larsen, K. Subramani:
Resource-Optimal Scheduling Using Priced Timed Automata. 220-235 - Pavel Krcál, Wang Yi:
Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata. 236-250
Constraint Solving
- Flemming Nielson, Hanne Riis Nielson, Hongyan Sun, Mikael Buchholtz, René Rydhof Hansen
The Succinct Solver Suite. 251-265 - Nathan Linger, Tim Sheard:
Binding-Time Analysis for MetaML via Type Inference and Constraint Solving. 266-279 - Zhendong Su
A Class of Polynomially Solvable Range Constraints for Interval Analysis without Widenings and Narrowings. 280-295
Timed Systems
- Denis Lugiez, Peter Niebert, Sarah Zennou:
A Partial Order Semantics Approach to the Clock Explosion Problem of Timed Automata. 296-311 - Gerd Behrmann, Patricia Bouyer, Kim Guldstrand Larsen, Radek Pelánek:
Lower and Upper Bounds in Zone Based Abstractions of Timed Automata. 312-326 - Stefan Leue, Richard Mayr, Wei Wei:
A Scalable Incomplete Test for the Boundedness of UML RT Models. 327-341 - Giorgio Delzanno, Pierre Ganty:
Automatic Verification of Time Sensitive Cryptographic Protocols. 342-356
Case Studies
- A. E. Lindsey, Charles Pecheur:
Simulation-Based Verification of Autonomous Controllers via Livingstone PathFinder. 357-371 - Danièle Beauquier, Tristan Crolard, Evguenia Prokofieva:
Automatic Parametric Verification of a Root Contention Protocol Based on Abstract State Machines and First Order Timed Logic. 372-387
Software
- Thomas Ball, Byron Cook, Satyaki Das, Sriram K. Rajamani:
Refining Approximations in Software Predicate Abstraction. 388-403 - Robby, Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff:
Checking Strong Specifications Using an Extensible Software Model Checking Framework. 404-420 - Samson Abramsky
Applying Game Semantics to Compositional Software Modeling and Verification. 421-435
Temporal Logic
- Jan Friso Groote
Solving Disjunctive/Conjunctive Boolean Equation Systems with Alternating Fixed Points. 436-450 - Arie Gurfinkel
How Vacuous Is Vacuous? 451-466 - Rajeev Alur, Kousha Etessami, P. Madhusudan:
A Temporal Logic of Nested Calls and Returns. 467-481 - Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck:
Liveness with Incomprehensible Ranking. 482-496
Abstraction
- Kairong Qian, Albert Nymeyer:
Guided Invariant Model Checking Based on Abstraction and Symbolic Pattern Databases. 497-511 - Denis Gopan, Frank DiMaio, Nurit Dor, Thomas W. Reps, Shmuel Sagiv:
Numeric Domains with Summarized Dimensions. 512-529 - Greta Yorsh, Thomas W. Reps, Shmuel Sagiv:
Symbolically Computing Most-Precise Abstract Operations for Shape Analysis. 530-545 - Sharon Shoham
Monotonic Abstraction-Refinement for CTL. 546-560
Automata Techniques
- Bernard Boigelot, Axel Legay, Pierre Wolper
Omega-Regular Model Checking. 561-575 - Sébastien Bardin, Alain Finkel, Jérôme Leroux:
FASTer Acceleration of Counter Automata in Practice. 576-590 - Orna Kupferman, Moshe Y. Vardi:
From Complementation to Certification. 591-606
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: