5. ATVA 2007:
Tokyo,
Japan
Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino, Yoshio Okamura (Eds.):
Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, Proceedings.
Lecture Notes in Computer Science 4762 Springer 2007, ISBN 978-3-540-75595-1 BibTeX
Invited Talks
Regular Papers
- Jörg Bauer, Tobe Toben, Bernd Westphal:
Mind the Shapes: Abstraction Refinement Via Topology Invariants.
35-50
Electronic Edition (link) BibTeX
- Geng-Dian Huang, Bow-Yaw Wang:
Complete SAT-Based Model Checking for Context-Free Processes.
51-65
Electronic Edition (link) BibTeX
- David Walter, Scott Little, Chris J. Myers:
Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver.
66-81
Electronic Edition (link) BibTeX
- Gordon J. Pace, Cristian Prisacariu, Gerardo Schneider:
Model Checking Contracts - A Case Study.
82-97
Electronic Edition (link) BibTeX
- Gilles Geeraerts, Jean-François Raskin, Laurent Van Begin:
On the Efficient Computation of the Minimal Coverability Set for Petri Nets.
98-113
Electronic Edition (link) BibTeX
- Scott Little, David Walter, Kevin Jones, Chris J. Myers:
Analog/Mixed-Signal Circuit Verification Using Models Generated from Simulation Traces.
114-128
Electronic Edition (link) BibTeX
- Bijan Alizadeh, Masahiro Fujita:
Automatic Merge-Point Detection for Sequential Equivalence Checking of System-Level and RTL Descriptions.
129-144
Electronic Edition (link) BibTeX
- Peter Habermehl, Radu Iosif, Adam Rogalewicz, Tomás Vojnar:
Proving Termination of Tree Manipulating Programs.
145-161
Electronic Edition (link) BibTeX
- Marco Bozzano, Alessandro Cimatti, Francesco Tapparo:
Symbolic Fault Tree Analysis for Reactive Systems.
162-176
Electronic Edition (link) BibTeX
- Thomas Gawlitza, Helmut Seidl:
Computing Game Values for Crash Games.
177-191
Electronic Edition (link) BibTeX
- Franck Cassez, Alexandre David, Kim Guldstrand Larsen, Didier Lime, Jean-François Raskin:
Timed Control with Observation Based and Stuttering Invariant Strategies.
192-206
Electronic Edition (link) BibTeX
- Lijun Zhang, Holger Hermanns:
Deciding Simulations on Probabilistic Automata.
207-222
Electronic Edition (link) BibTeX
- Christian Dax, Jochen Eisinger, Felix Klaedtke:
Mechanizing the Powerset Construction for Restricted Classes of omega -Automata.
223-236
Electronic Edition (link) BibTeX
- Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti:
Verifying Heap-Manipulating Programs in an SMT Framework.
237-252
Electronic Edition (link) BibTeX
- Sophie Pinchinat:
A Generic Constructive Solution for Concurrent Games with Expressive Constraints on Strategies.
253-267
Electronic Edition (link) BibTeX
- Sven Schewe, Bernd Finkbeiner:
Distributed Synthesis for Alternating-Time Logics.
268-283
Electronic Edition (link) BibTeX
- Indranil Saha, Janardan Misra, Suman Roy:
Timeout and Calendar Based Finite State Modeling and Verification of Real-Time Systems.
284-299
Electronic Edition (link) BibTeX
- Dragan Bosnacki, Alastair F. Donaldson, Michael Leuschel, Thierry Massart:
Efficient Approximate Verification of Promela Models Via Symmetry Markers.
300-315
Electronic Edition (link) BibTeX
- Orna Kupferman, Yoad Lustig:
Latticed Simulation Relations and Games.
316-330
Electronic Edition (link) BibTeX
- Tingting Han, Joost-Pieter Katoen:
Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking.
331-346
Electronic Edition (link) BibTeX
- Judi Romijn, Wieger Wesselink, Arjan J. Mooij:
Assertion-Based Proof Checking of Chang-Roberts Leader Election in PVS.
347-361
Electronic Edition (link) BibTeX
- Laura Recalde, Serge Haddad, Manuel Silva:
Continuous Petri Nets: Expressive Power and Decidability Issues.
362-377
Electronic Edition (link) BibTeX
- Edith Elkind, Blaise Genest, Doron Peled, Paola Spoletini:
Quantifying the Discord: Order Discrepancies in Message Sequence Charts.
378-393
Electronic Edition (link) BibTeX
- Ismael Rodríguez, Manuel Núñez:
A Formal Methodology to Test Complex Heterogeneous Systems.
394-409
Electronic Edition (link) BibTeX
- Rotem Oshman, Orna Grumberg:
A New Approach to Bounded Model Checking for Branching Time Logics.
410-424
Electronic Edition (link) BibTeX
- Werner Damm, Stefan Disch, Hardi Hungar, Swen Jacobs, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz:
Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space.
425-440
Electronic Edition (link) BibTeX
- Hichem Boudali, Pepijn Crouzen, Mariëlle Stoelinga:
A Compositional Semantics for Dynamic Fault Trees in Terms of Interactive Markov Chains.
441-456
Electronic Edition (link) BibTeX
- Orna Grumberg, Assaf Schuster, Avi Yadgar:
3-Valued Circuit SAT for STE with Automatic Refinement.
457-473
Electronic Edition (link) BibTeX
- Sven Schewe, Bernd Finkbeiner:
Bounded Synthesis.
474-488
Electronic Edition (link) BibTeX
Short Papers
- Moonzoo Kim:
Formal Modeling and Verification of High-Availability Protocol for Network Security Appliances.
489-500
Electronic Edition (link) BibTeX
- Mercedes G. Merayo, Manuel Núñez, Ismael Rodríguez:
A Brief Introduction to THOTL.
501-510
Electronic Edition (link) BibTeX
- Guoqiang Li, Mizuhito Ogawa:
On-the-Fly Model Checking of Fair Non-repudiation Protocols.
511-522
Electronic Edition (link) BibTeX
- Bernard Berthomieu, Florent Peres, François Vernadat:
Model Checking Bounded Prioritized Time Petri Nets.
523-532
Electronic Edition (link) BibTeX
- Salamah Salamah, Ann Q. Gates, Vladik Kreinovich, Steve Roach:
Using Patterns and Composite Propositions to Automate the Generation of LTL Specifications.
533-542
Electronic Edition (link) BibTeX
- Muhammad Torabi Dashti, Anton Wijs:
Pruning State Spaces with Extended Beam Search.
543-552
Electronic Edition (link) BibTeX
- Thanyapat Sakunkonchak, Satoshi Komatsu, Masahiro Fujita:
Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction.
553-563
Electronic Edition (link) BibTeX
Copyright © Thu Jan 1 17:07:09 2009
by Michael Ley (ley@uni-trier.de)
