13. TACAS 2007: Braga, Portugal (Part of ETAPS 2007)

Orna Grumberg, Michael Huth (Eds.): Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings. Lecture Notes in Computer Science 4424 Springer 2007, ISBN 978-3-540-71208-4 BibTeX

Invited Contributions

Rance Cleaveland:
THERE AND BACK AGAIN: Lessons Learned on the Way to the Market. 1
Electronic Edition (link) BibTeX
K. Rustan M. Leino:
Verifying Object-Oriented Software: Lessons and Challenges. 2
Electronic Edition (link) BibTeX

Software Verification

Roman Manevich, Josh Berdine, Byron Cook, G. Ramalingam, Mooly Sagiv:
Shape Analysis by Graph Decomposition. 3-18
Electronic Edition (link) BibTeX
Shaunak Chatterjee, Shuvendu K. Lahiri, Shaz Qadeer, Zvonimir Rakamaric:
A Reachability Predicate for Analyzing Low-Level Software. 19-33
Electronic Edition (link) BibTeX
Muhammad Zubair Malik, Aman Pervaiz, Sarfraz Khurshid:
Generating Representation Invariants of Structurally Complex Data. 34-49
Electronic Edition (link) BibTeX

Probabilistic Model Checking and Markov Chains

Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, Mihalis Yannakakis:
Multi-objective Model Checking of Markov Decision Processes. 50-65
Electronic Edition (link) BibTeX
Dominik Wojtczak, Kousha Etessami:
PReMo : An Analyzer for P robabilistic Re cursive Mo dels. 66-71
Electronic Edition (link) BibTeX
Tingting Han, Joost-Pieter Katoen:
Counterexamples in Probabilistic Model Checking. 72-86
Electronic Edition (link) BibTeX
Joost-Pieter Katoen, Tim Kemna, Ivan S. Zapreev, David N. Jansen:
Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking. 87-101
Electronic Edition (link) BibTeX

Static Analysis

Azadeh Farzan, P. Madhusudan:
Causal Dataflow Analysis for Concurrent Programs. 102-116
Electronic Edition (link) BibTeX
Saswat Anand, Alessandro Orso, Mary Jean Harrold:
Type-Dependence Analysis and Program Transformation for Symbolic Execution. 117-133
Electronic Edition (link) BibTeX
Saswat Anand, Corina S. Pasareanu, Willem Visser:
JPF-SE: A Symbolic Execution Extension to Java PathFinder. 134-138
Electronic Edition (link) BibTeX

Markov Chains and Real-Time Systems

Salem Derisavi:
A Symbolic Algorithm for Optimal Markov Chain Lumping. 139-154
Electronic Edition (link) BibTeX
Lijun Zhang, Holger Hermanns, Friedrich Eisenbrand, David N. Jansen:
Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations. 155-169
Electronic Edition (link) BibTeX
Marcin Jurdzinski, François Laroussinie, Jeremy Sproston:
Model Checking Probabilistic Timed Automata with One or Two Clocks. 170-184
Electronic Edition (link) BibTeX
Massimo Tivoli, Pascal Fradet, Alain Girault, Gregor Gößler:
Adaptor Synthesis for Real-Time Components. 185-200
Electronic Edition (link) BibTeX

Timed Automata and Duration Calculus

Martin Fränzle, Michael R. Hansen:
Deciding an Interval Logic with Accumulated Durations. 201-215
Electronic Edition (link) BibTeX
Davide D'Aprile, Susanna Donatelli, Arnaud Sangnier, Jeremy Sproston:
From Time Petri Nets to Timed Automata: An Untimed Approach. 216-230
Electronic Edition (link) BibTeX
Jacob Illum Rasmussen, Gerd Behrmann, Kim Guldstrand Larsen:
Complexity in Simplicity: Flexible Agent-Based State Space Exploration. 231-245
Electronic Edition (link) BibTeX
Paritosh K. Pandya, Shankara Narayanan Krishna, Kuntal Loya:
On Sampling Abstraction of Continuous Time Logic with Durations. 246-260
Electronic Edition (link) BibTeX

Assume-Guarantee Reasoning

Krishnendu Chatterjee, Thomas A. Henzinger:
Assume-Guarantee Synthesis. 261-275
Electronic Edition (link) BibTeX
Sagar Chaki, Ofer Strichman:
Optimized L*-Based Assume-Guarantee Reasoning. 276-291
Electronic Edition (link) BibTeX
Mihaela Gheorghiu, Dimitra Giannakopoulou, Corina S. Pasareanu:
Refining Interface Alphabets for Compositional Verification. 292-307
Electronic Edition (link) BibTeX
Max Goldman, Shmuel Katz:
MAVEN: Modular Aspect Verification. 308-322
Electronic Edition (link) BibTeX

Biological Systems

Grégory Batt, Calin Belta, Ron Weiss:
Model Checking Liveness Properties of Genetic Regulatory Networks. 323-338
Electronic Edition (link) BibTeX
Panagiotis Manolios, Marc Galceran Oms, Sergi Oliva Valls:
Checking Pedigree Consistency with PCS. 339-342
Electronic Edition (link) BibTeX
Hillel Kugler, Amir Pnueli, Michael J. Stern, E. Jane Albert Hubbard:
"Don't Care" Modeling: A Logical Framework for Developing Predictive System Models. 343-357
Electronic Edition (link) BibTeX

Abstraction Refinement

Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady:
Deciding Bit-Vector Arithmetic with Abstraction. 358-372
Electronic Edition (link) BibTeX
Alessandro Armando, Massimo Benerecetti, Jacopo Mantovani:
Abstraction Refinement of Linear Programs with Arrays. 373-388
Electronic Edition (link) BibTeX
Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi:
Property-Driven Partitioning for Abstraction Refinement. 389-404
Electronic Edition (link) BibTeX
Nina Amla, Kenneth L. McMillan:
Combining Abstraction Refinement and SAT-Based Model Checking. 405-419
Electronic Edition (link) BibTeX

Message Sequence Charts

Edith Elkind, Blaise Genest, Doron Peled:
Detecting Races in Ensembles of Message Sequence Charts. 420-434
Electronic Edition (link) BibTeX
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker:
Replaying Play In and Play Out: Synthesis of Design Models from Scenarios by Learning. 435-450
Electronic Edition (link) BibTeX

Automata-Based Model Checking

Laurent Doyen, Jean-François Raskin:
Improved Algorithms for the Automata-Based Approach to Model-Checking. 451-465
Electronic Edition (link) BibTeX
Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Kang-Nien Wu, Wen-Chin Chan:
GOAL: A Graphical Tool for Manipulating Büchi Automata and Temporal Formulae. 466-471
Electronic Edition (link) BibTeX
Florian Horn:
Faster Algorithms for Finitary Games. 472-484
Electronic Edition (link) BibTeX

Specification Languages

David Harel, Itai Segall:
Planned and Traversable Play-Out: A Flexible Method for Executing Scenario-Based Programs^,. 485-499
Electronic Edition (link) BibTeX
Henrik C. Bohnenkamp, Holger Hermanns, Joost-Pieter Katoen:
motor: The modestTool Environment. 500-504
Electronic Edition (link) BibTeX
Alessandro Cimatti, Marco Roveri, Stefano Tonetta:
Syntactic Optimizations for PSL Verification. 505-518
Electronic Edition (link) BibTeX
Till Mossakowski, Christian Maeder, Klaus Lüttich:
The Heterogeneous Tool Set, Hets. 519-522
Electronic Edition (link) BibTeX

Security

Shaddin F. Doghmi, Joshua D. Guttman, F. Javier Thayer:
Searching for Shapes in Cryptographic Protocols. 523-537
Electronic Edition (link) BibTeX
Véronique Cortier, Gavin Keighren, Graham Steel:
Automatic Analysis of the Security of XOR-Based Key Management Schemes. 538-552
Electronic Edition (link) BibTeX

Software and Hardware Verification

Ranjit Jhala, Rupak Majumdar, Ru-Gang Xu:
State of the Union: Type Inference Via Craig Interpolation. 553-567
Electronic Edition (link) BibTeX
Magnus O. Myreen, Michael J. C. Gordon:
Hoare Logic for Realistically Modelled Machine Code. 568-582
Electronic Edition (link) BibTeX
Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke:
VCEGAR: Verilog CounterExample Guided Abstraction Refinement. 583-586
Electronic Edition (link) BibTeX

Decision Procedures and Theorem Provers

Marcelo F. Frias, Carlos López Pombo, Mariano M. Moscato:
Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications. 587-601
Electronic Edition (link) BibTeX
Sava Krstic, Amit Goel, Jim Grundy, Cesare Tinelli:
Combined Satisfiability Modulo Parametric Theories. 602-617
Electronic Edition (link) BibTeX
Christopher Condrat, Priyank Kalla:
A Gröbner Basis Approach to CNF-Formulae Preprocessing. 618-631
Electronic Edition (link) BibTeX
Emina Torlak, Daniel Jackson:
Kodkod: A Relational Model Finder. 632-647
Electronic Edition (link) BibTeX

Model Checking

Andy Jinqing Yu, Gianfranco Ciardo, Gerald Lüttgen:
Bounded Reachability Checking of Asynchronous Systems Using Decision Diagrams. 648-663
Electronic Edition (link) BibTeX
Rajeev Alur, Pavol Cerný, Swarat Chaudhuri:
Model Checking on Trees with Path Equivalences. 664-678
Electronic Edition (link) BibTeX
Sebastian Kupferschmid, Klaus Dräger, Jörg Hoffmann, Bernd Finkbeiner, Henning Dierks, Andreas Podelski, Gerd Behrmann:
Uppaal/DMC- Abstraction-Based Heuristics for Directed Model Checking. 679-682
Electronic Edition (link) BibTeX
Stefan Blom, Jens R. Calame, Bert Lisser, Simona Orzan, Jun Pang, Jaco van de Pol, Muhammad Torabi Dashti, Anton Wijs:
Distributed Analysis with mu CRL: A Compendium of Case Studies. 683-689
Electronic Edition (link) BibTeX

Infinite-State Systems

Ahmed Bouajjani, Yan Jurski, Mihaela Sighireanu:
A Generic Framework for Reasoning About Dynamic Networks of Infinite-State Processes. 690-705
Electronic Edition (link) BibTeX
Frédéric Herbreteau, Grégoire Sutre, The Quang Tran:
Unfolding Concurrent Well-Structured Transition Systems. 706-720
Electronic Edition (link) BibTeX
Parosh Aziz Abdulla, Giorgio Delzanno, Noomene Ben Henda, Ahmed Rezine:
Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems). 721-736
Electronic Edition (link) BibTeX