5. ATVA 2007: Tokyo, Japan

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 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:
  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
  
• 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
  

Last update Tue May 22 23:22:59 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page