Abstract is missing.
- Ranking Abstraction as a Companion to Predicate Abstraction, Amir Pnueli. 1 [doi]
- Termination and Invariance Analysis of LoopsAaron R. Bradley, Zohar Manna. 2 [doi]
- Some Perspectives of Infinite-State VerificationWolfgang Thomas. 3-10 [doi]
- Verifying Very Large Industrial Circuits Using 100 Processes and BeyondLimor Fix, Orna Grumberg, Amnon Heyman, Tamir Heyman, Assaf Schuster. 11-25 [doi]
- A New Reachability Algorithm for Symmetric Multi-processor ArchitectureDebashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill. 26-38 [doi]
- Comprehensive Verification Framework for Dependability of Self-optimizing SystemsYuhong Zhao, Martin Kardos, Simon Oberthür, Franz J. Rammig. 39-53 [doi]
- Exploiting Hub States in Automatic VerificationGiuseppe Della Penna, Igor Melatti, Benedetto Intrigila, Enrico Tronci. 54-68 [doi]
- An Approach for the Verification of SystemC Designs Using AsmLAli Habibi, Sofiène Tahar. 69-83 [doi]
- Decomposition-Based Verification of Cyclic WorkflowsYongsun Choi, J. Leon Zhao. 84-98 [doi]
- Guaranteed Termination in the Verification of LTL Properties of Non-linear Robust Discrete Time Hybrid SystemsWerner Damm, Guilherme Pinto, Stefan Ratschan. 99-113 [doi]
- Computation Platform for Automatic Analysis of Embedded Software Systems Using Model Based ApproachA. Dubey, X. Wu, H. Su, T. J. Koo. 114-128 [doi]
- Quantitative and Qualitative Analysis of Temporal Aspects of Complex ActivitiesAndrei Voinikonis. 129-143 [doi]
- Automatic Test Case Generation with Region-Related Coverage Annotations for Real-Time SystemsGeng-Dian Huang, Farn Wang. 144-158 [doi]
- Selective Search in Bounded Model Checking of Reachability PropertiesMaciej Szreter. 159-173 [doi]
- Predicate Abstraction of RTL Verilog Descriptions Using Constraint Logic ProgrammingTun Li, Yang Guo, Sikun Li, Gongjie Liu. 174-186 [doi]
- State Space Exploration of Object-Based Systems Using Equivalence Reduction and the Sweepline MethodCharles A. Lakos, Lars Michael Kristensen. 187-201 [doi]
- Syntactical Colored Petri Nets ReductionsSami Evangelista, Serge Haddad, Jean-François Pradat-Peyre. 202-216 [doi]
- Algorithmic Algebraic Model Checking II: Decidability of Semi-algebraic Model Checking and Its Applications to Systems BiologyVenkatesh Mysore, Carla Piazza, Bud Mishra. 217-233 [doi]
- A Static Analysis Using Tree Automata for XML Access ControlIsao Yagi, Yoshiaki Takata, Hiroyuki Seki. 234-247 [doi]
- Reasoning About Transfinite SequencesStéphane Demri, David Nowak. 248-262 [doi]
- Semi-automatic Distributed SynthesisBernd Finkbeiner, Sven Schewe. 263-277 [doi]
- A New Graph of Classes for the Preservation of Quantitative Temporal ConstraintsXiaoyu Mao, Janette Cardoso, Robert Valette. 278-292 [doi]
- Comparison of Different Semantics for Time Petri NetsBéatrice Bérard, Franck Cassez, Serge Haddad, Didier Lime, Olivier H. Roux. 293-307 [doi]
- Introducing Dynamic Properties with Past Temporal Operators in the B RefinementMouna Saad, Leila Jemni Ben Ayed. 308-322 [doi]
- Approximate Reachability for Dead Code Elimination in EsterelOlivier Tardieu, Stephen A. Edwards. 323-337 [doi]
- Synthesis of Interface AutomataPurandar Bhaduri. 338-353 [doi]
- Multi-valued Model Checking GamesSharon Shoham, Orna Grumberg. 354-369 [doi]
- Model Checking Prioritized Timed AutomataShang-Wei Lin, Pao-Ann Hsiung, Chun-Hsian Huang, Yean-Ru Chen. 370-384 [doi]
- An MTBDD-Based Implementation of Forward Reachability for Probabilistic Timed AutomataFuzhi Wang, Marta Z. Kwiatkowska. 385-399 [doi]
- An EFSM-Based Intrusion Detection System for Ad Hoc NetworksJean-Marie Orset, Baptiste Alcalde, Ana R. Cavalli. 400-413 [doi]
- Modeling and Verification of a Telecommunication Application Using Live Sequence Charts and the Play-Engine ToolPierre Combes, David Harel, Hillel Kugler. 414-428 [doi]
- Formal Construction and Verification of Home Service Robots: A Case StudyMoonzoo Kim, Kyo Chul Kang. 429-443 [doi]
- Model Checking Real Time Java Using Java PathFinderGary Lindstrom, Peter C. Mehlitz, Willem Visser. 444-456 [doi]
- Using Parametric Automata for the Verification of the Stop-and-Wait Class of ProtocolsGuy Edward Gallasch, Jonathan Billington. 457-473 [doi]
- Flat Acceleration in Symbolic Model CheckingSébastien Bardin, Alain Finkel, Jérôme Leroux, Ph. Schnoebelen. 474-488 [doi]
- Flat Counter Automata Almost Everywhere!Jérôme Leroux, Grégoire Sutre. 489-503 [doi]