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

Invited Contributions

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

Software Verification

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

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
Dominik Wojtczak, Kousha Etessami:
PReMo : An Analyzer for P robabilistic Re cursive Mo dels. 66-71
Tingting Han, Joost-Pieter Katoen:
Counterexamples in Probabilistic Model Checking. 72-86
Joost-Pieter Katoen, Tim Kemna, Ivan S. Zapreev, David N. Jansen:
Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking. 87-101

Static Analysis

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

Markov Chains and Real-Time Systems

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

Timed Automata and Duration Calculus

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

Assume-Guarantee Reasoning

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

Biological Systems

Grégory Batt, Calin Belta, Ron Weiss:
Model Checking Liveness Properties of Genetic Regulatory Networks. 323-338
Panagiotis Manolios, Marc Galceran Oms, Sergi Oliva Valls:
Checking Pedigree Consistency with PCS. 339-342
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

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
Alessandro Armando, Massimo Benerecetti, Jacopo Mantovani:
Abstraction Refinement of Linear Programs with Arrays. 373-388
Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi:
Property-Driven Partitioning for Abstraction Refinement. 389-404
Nina Amla, Kenneth L. McMillan:
Combining Abstraction Refinement and SAT-Based Model Checking. 405-419

Message Sequence Charts

Edith Elkind, Blaise Genest, Doron Peled:
Detecting Races in Ensembles of Message Sequence Charts. 420-434
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

Automata-Based Model Checking

Laurent Doyen, Jean-François Raskin:
Improved Algorithms for the Automata-Based Approach to Model-Checking. 451-465
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
Florian Horn:
Faster Algorithms for Finitary Games. 472-484

Specification Languages

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

Security

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

Software and Hardware Verification

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

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
Sava Krstic, Amit Goel, Jim Grundy, Cesare Tinelli:
Combined Satisfiability Modulo Parametric Theories. 602-617
Christopher Condrat, Priyank Kalla:
A Gröbner Basis Approach to CNF-Formulae Preprocessing. 618-631
Emina Torlak, Daniel Jackson:
Kodkod: A Relational Model Finder. 632-647

Model Checking

Andy Jinqing Yu, Gianfranco Ciardo, Gerald Lüttgen:
Bounded Reachability Checking of Asynchronous Systems Using Decision Diagrams. 648-663
Rajeev Alur, Pavol Cerný, Swarat Chaudhuri:
Model Checking on Trees with Path Equivalences. 664-678
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
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

Infinite-State Systems

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

Last update Wed Feb 15 05:19:08 2012 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page