default search action
14th TACAS 2008: Budapest, Hungary (Part of ETAPS 2008)
- C. R. Ramakrishnan, Jakob Rehof:
Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. Lecture Notes in Computer Science 4963, Springer 2008, ISBN 978-3-540-78799-0
Invited Talk
- Sharad Malik:
Hardware Verification: Techniques, Methodology and Solutions. 1
Parameterized Systems
- Azadeh Farzan, Yu-Fang Chen, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang:
Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages. 2-17 - Mayank Saksena, Oskar Wibling, Bengt Jonsson:
Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols. 18-32 - Edmund M. Clarke, Muralidhar Talupur, Helmut Veith:
Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems. 33-47
Model Checking - I
- Jiri Barnat, Lubos Brim, Pavel Simecek, M. Weber:
Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. 48-62 - Martin De Wulf, Laurent Doyen, Nicolas Maquet, Jean-François Raskin:
Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking. 63-77 - Adam Bakewell, Dan R. Ghica:
On-the-Fly Techniques for Game-Based Software Model Checking. 78-92 - Parosh Aziz Abdulla, Ahmed Bouajjani, Lukás Holík, Lisa Kaati, Tomás Vojnar:
Computing Simulations over Tree Automata. 93-108
Applications
- Eyad Alkassar, Norbert Schirmer, Artem Starostin:
Formal Pervasive Verification of a Paging Mechanism. 109-123 - Gogul Balakrishnan, Thomas W. Reps:
Analyzing Stripped Device-Driver Executables. 124-140 - Gal Katz, Doron A. Peled:
Model Checking-Based Genetic Programming with an Application to Mutual Exclusion. 141-156
Model Checking - II
- Miguel E. Andrés, Peter van Rossum:
Conditional Probabilities over Probabilistic and Nondeterministic Systems. 157-172 - Axel Legay, Andrzej S. Murawski, Joël Ouaknine, James Worrell:
On Automated Verification of Probabilistic Programs. 173-187 - Sriram Sankaranarayanan, Thao Dang, Franjo Ivancic:
Symbolic Model Checking of Hybrid Systems Using Template Polyhedra. 188-202 - Sebastian Kupferschmid, Jörg Hoffmann, Kim Guldstrand Larsen:
Fast Directed Model Checking Via Russian Doll Abstraction. 203-217
Static Analysis
- Amir M. Ben-Amram, Michael Codish:
A SAT-Based Approach to Size Change Termination with Global Ranking Functions. 218-232 - Hana Chockler, Orna Grumberg, Avi Yadgar:
Efficient Automatic STE Refinement Using Responsibility. 233-248 - Laura Kovács:
Reasoning Algebraically About P-Solvable Loops. 249-264 - Carsten Ihlemann, Swen Jacobs, Viorica Sofronie-Stokkermans:
On Local Reasoning in Verification. 265-281
Concurrent/Distributed Systems
- Akash Lal, Tayssir Touili, Nicholas Kidd, Thomas W. Reps:
Interprocedural Analysis of Concurrent Programs Under a Context Bound. 282-298 - Salvatore La Torre, P. Madhusudan, Gennaro Parlato:
Context-Bounded Analysis of Concurrent Queue Systems. 299-314 - Dana Fisman, Orna Kupferman, Yoad Lustig:
On Verifying Fault Tolerance of Distributed Protocols. 315-331
Tools - I
- Peter Csaba Ölveczky, José Meseguer:
The Real-Time Maude Tool. 332-336 - Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Z3: An Efficient SMT Solver. 337-340 - Gordon J. Pace, Gerardo Schneider:
Computation and Visualisation of Phase Portraits for Model Checking SPDIs. 341-345 - Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Wen-Chin Chan, Chi-Jian Luo:
GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic. 346-350
Symbolic Execution
- Peter Boonstoppel, Cristian Cadar, Dawson R. Engler:
RWset: Attacking Path Explosion in Constraint-Based Test Generation. 351-366 - Saswat Anand, Patrice Godefroid, Nikolai Tillmann:
Demand-Driven Compositional Symbolic Execution. 367-381 - Chao Wang, Zijiang Yang, Vineet Kahlon, Aarti Gupta:
Peephole Partial Order Reduction. 382-396
Abstraction, Interpolation
- Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani:
Efficient Interpolant Generation in Satisfiability Modulo Theories. 397-412 - Kenneth L. McMillan:
Quantified Invariant Generation Using an Interpolating Saturation Prover. 413-427 - Nicolas Caniart, Emmanuel Fleury, Jérôme Leroux, Marc Zeitoun:
Accelerating Interpolation-Based Model-Checking. 428-442 - Bhargav S. Gulavani, Supratik Chakraborty, Aditya V. Nori, Sriram K. Rajamani:
Automatically Refining Abstract Interpretations. 443-458
Tools - II
- Thomas Wahl, Nicolas Blanc, E. Allen Emerson:
SVISS: Symbolic Verification of Symmetric Systems. 459-462 - Bernd Finkbeiner, Hans-Jörg Peter, Sven Schewe:
RESY: Requirement Synthesis for Compositional Model Checking. 463-466 - Nicolas Blanc, Daniel Kroening, Natasha Sharygina:
Scoot: A Tool for the Analysis of SystemC Models. 467-470
Trust, Reputation
- Guodong Li, Konrad Slind:
Trusted Source Translation of a Total Function Language. 471-485 - Michal Moskal:
Rocket-Fast Proof Checking for SMT Solvers. 486-500 - Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Dejvuth Suwimonteerabuth:
SDSIrep: A Reputation System Based on SDSI. 501-516
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.