default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID5th ATVA 2007: Tokyo, Japan
- Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino, Yoshio Okamura:
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
Invited Talks
- Nathan Whitehead, Jordan Johnson, Martín Abadi:
Policies and Proofs for Code Auditing. 1-14 - 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 - Sumit Nain, Moshe Y. Vardi:
Branching vs. Linear Time: Semantical Perspective. 19-34
Regular Papers
- Jörg Bauer, Tobe Toben, Bernd Westphal:
Mind the Shapes: Abstraction Refinement Via Topology Invariants. 35-50 - Geng-Dian Huang, Bow-Yaw Wang:
Complete SAT-Based Model Checking for Context-Free Processes. 51-65 - 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 - Thomas Gawlitza, Helmut Seidl:
Computing Game Values for Crash Games. 177-191 - Franck Cassez, Alexandre David, Kim Guldstrand Larsen, Didier Lime, Jean-François Raskin:
Timed Control with Observation Based and Stuttering Invariant Strategies. 192-206 - Lijun Zhang, Holger Hermanns:
Deciding Simulations on Probabilistic Automata. 207-222 - 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 - Sven Schewe, Bernd Finkbeiner:
Distributed Synthesis for Alternating-Time Logics. 268-283 - 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 - Orna Kupferman, Yoad Lustig:
Latticed Simulation Relations and Games. 316-330 - 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 Suárez:
Continuous Petri Nets: Expressive Power and Decidability Issues. 362-377 - Edith Elkind, Blaise Genest, Doron A. Peled, Paola Spoletini:
Quantifying the Discord: Order Discrepancies in Message Sequence Charts. 378-393 - Ismael Rodríguez, Manuel Núñez:
A Formal Methodology to Test Complex Heterogeneous Systems. 394-409 - 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 - Sven Schewe, Bernd Finkbeiner:
Bounded Synthesis. 474-488
Short Papers
- Moonzoo Kim:
Formal Modeling and Verification of High-Availability Protocol for Network Security Appliances. 489-500 - Mercedes G. Merayo, Manuel Núñez, Ismael Rodríguez:
A Brief Introduction to THOTL. 501-510 - Guoqiang Li, Mizuhito Ogawa:
On-the-Fly Model Checking of Fair Non-repudiation Protocols. 511-522 - 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 - Muhammad Torabi Dashti, Anton Wijs:
Pruning State Spaces with Extended Beam Search. 543-552 - Thanyapat Sakunkonchak, Satoshi Komatsu, Masahiro Fujita:
Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction. 553-563
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.
last updated on 2025-03-29 00:04 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
