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. Springer 2007 Lecture Notes in Computer Science ISBN 978-3-540-75595-1
Invited Talks
- Atsushi Hasegawa: Recent Trend in Industry and Expectation to DA Research. 15-16
- Kenneth L. McMillan: Toward Property-Driven Abstraction for Heap Manipulating Programs. 17-18
Regular Papers
- Jörg Bauer, Tobe Toben, Bernd Westphal: Mind the Shapes: Abstraction Refinement Via Topology Invariants. 35-50
- David Walter, Scott Little, Chris J. Myers: Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver. 66-81
- Gordon J. Pace, Cristian Prisacariu, Gerardo Schneider: Model Checking Contracts - A Case Study. 82-97
- Gilles Geeraerts, Jean-François Raskin, Laurent Van Begin: On the Efficient Computation of the Minimal Coverability Set for Petri Nets. 98-113
- Scott Little, David Walter, Kevin R. Jones, Chris J. Myers: Analog/Mixed-Signal Circuit Verification Using Models Generated from Simulation Traces. 114-128
- Bijan Alizadeh, Masahiro Fujita: Automatic Merge-Point Detection for Sequential Equivalence Checking of System-Level and RTL Descriptions. 129-144
- Peter Habermehl, Radu Iosif, Adam Rogalewicz, Tomás Vojnar: Proving Termination of Tree Manipulating Programs. 145-161
- Marco Bozzano, Alessandro Cimatti, Francesco Tapparo: Symbolic Fault Tree Analysis for Reactive Systems. 162-176
- Franck Cassez, Alexandre David, Kim Guldstrand Larsen, Didier Lime, Jean-François Raskin: Timed Control with Observation Based and Stuttering Invariant Strategies. 192-206
- Christian Dax, Jochen Eisinger, Felix Klaedtke: Mechanizing the Powerset Construction for Restricted Classes of omega -Automata. 223-236
- Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti: Verifying Heap-Manipulating Programs in an SMT Framework. 237-252
- Sophie Pinchinat: A Generic Constructive Solution for Concurrent Games with Expressive Constraints on Strategies. 253-267
- Indranil Saha, Janardan Misra, Suman Roy: Timeout and Calendar Based Finite State Modeling and Verification of Real-Time Systems. 284-299
- Dragan Bosnacki, Alastair F. Donaldson, Michael Leuschel, Thierry Massart: Efficient Approximate Verification of Promela Models Via Symmetry Markers. 300-315
- Tingting Han, Joost-Pieter Katoen: Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking. 331-346
- Judi Romijn, Wieger Wesselink, Arjan J. Mooij: Assertion-Based Proof Checking of Chang-Roberts Leader Election in PVS. 347-361
- Laura Recalde, Serge Haddad, Manuel Silva: Continuous Petri Nets: Expressive Power and Decidability Issues. 362-377
- Edith Elkind, Blaise Genest, Doron Peled, Paola Spoletini: Quantifying the Discord: Order Discrepancies in Message Sequence Charts. 378-393
- Rotem Oshman, Orna Grumberg: A New Approach to Bounded Model Checking for Branching Time Logics. 410-424
- 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
- Hichem Boudali, Pepijn Crouzen, Mariëlle Stoelinga: A Compositional Semantics for Dynamic Fault Trees in Terms of Interactive Markov Chains. 441-456
- Orna Grumberg, Assaf Schuster, Avi Yadgar: 3-Valued Circuit SAT for STE with Automatic Refinement. 457-473
Short Papers
- Moonzoo Kim: Formal Modeling and Verification of High-Availability Protocol for Network Security Appliances. 489-500
- Bernard Berthomieu, Florent Peres, François Vernadat: Model Checking Bounded Prioritized Time Petri Nets. 523-532
- Salamah Salamah, Ann Q. Gates, Vladik Kreinovich, Steve Roach: Using Patterns and Composite Propositions to Automate the Generation of LTL Specifications. 533-542
- Thanyapat Sakunkonchak, Satoshi Komatsu, Masahiro Fujita: Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction. 553-563
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-18T214307 by the dblp team