Abstract is missing.
- Games for Formal Design and Verification of Reactive SystemsRajeev Alur. 1 [doi]
- Evolution of Model Checking into the EDA IndustryRobert P. Kurshan. 2-6 [doi]
- Abstraction RefinementPei-Hsin Ho. 7 [doi]
- Tools for Automated Verification of Web ServicesTevfik Bultan, Xiang Fu, Jianwen Su. 8-10 [doi]
- Theorem Proving Languages for VerificationJean-Pierre Jouannaud. 11-14 [doi]
- An Automated Rigorous Review Method for Verifying and Validating Formal SpecificationsShaoying Liu. 15-19 [doi]
- Toward Unbounded Model Checking for Region AutomataFang Yu, Bow-Yaw Wang. 20-33 [doi]
- Search Space Partition and Case Basis Exploration for Reducing Model Checking ComplexityBai Su, Wenhui Zhang. 34-48 [doi]
- Synthesising Attacks on Cryptographic ProtocolsDavid Sinclair, David Gray, Geoff Hamilton. 49-63 [doi]
- Büchi Complementation Made TighterEhud Friedgut, Orna Kupferman, Moshe Y. Vardi. 64-78 [doi]
- SAT-Based Verification of Safe Petri NetsShougo Ogata, Tatsuhiro Tsuchiya, Tohru Kikuno. 79-92 [doi]
- Disjunctive Invariants for Numerical SystemsJérôme Leroux. 93-107 [doi]
- Validity Checking for Quantifier-Free First-Order Logic with Equality Using Substitution of Boolean FormulasAtsushi Moritomo, Kiyoharu Hamaguchi, Toshinobu Kashiwabara. 108-119 [doi]
- Fair Testing Revisited: A Process-Algebraic Characterisation of ConflictsRobi Malik, David Streader, Steve Reeves. 120-134 [doi]
- Exploiting Symmetries for Testing Equivalence in the Spi CalculusIvan Cibrario Bertolotti, Luca Durante, Riccardo Sisto, Adriano Valenzano. 135-149 [doi]
- Using Block-Local Atomicity to Detect Stale-Value Concurrency ErrorsCyrille Artho, Klaus Havelund, Armin Biere. 150-164 [doi]
- Abstraction-Based Model Checking Using Heuristical RefinementKairong Qian, Albert Nymeyer. 165-178 [doi]
- A Global Timed Bisimulation Preserving Abstraction for Parametric Time-Interval AutomataTadaaki Tanimoto, Suguru Sasaki, Akio Nakata, Teruo Higashino. 179-195 [doi]
- Design and Evaluation of a Symbolic and Abstraction-Based Model CheckerSerge Haddad, Jean-Michel Ilié, Kais Klai. 196-210 [doi]
- Component-Wise Instruction-Cache Behavior PredictionAbdur Rakib, Oleg Parshin, Stephan Thesing, Reinhard Wilhelm. 211-229 [doi]
- Validating the Translation of an Industrial Optimizing CompilerI. Gordin, Raya Leviathan, Amir Pnueli. 230-247 [doi]
- Composition of Accelerations to Verify Infinite Heterogeneous SystemsSébastien Bardin, Alain Finkel. 248-262 [doi]
- Hybrid System Verification Is Not a Sinecure: The Electronic Throttle Control Case StudyAnsgar Fehnker, Bruce H. Krogh. 263-277 [doi]
- Providing Automated Verification in HOL Using MDGsTarek Mhamdi, Sofiène Tahar. 278-293 [doi]
- Specification, Abduction, and ProofKonstantine Arkoudas. 294-309 [doi]
- Introducing Structural Dynamic Changes in Petri Nets: Marked-Controlled Reconfigurable NetsMarisa Llorens, Javier Oliver. 310-323 [doi]
- Typeness for omega-Regular AutomataOrna Kupferman, Gila Morgenstern, Aniello Murano. 324-338 [doi]
- Partial Order Reduction for Detecting Safety and Timing Failures of Timed CircuitsDenduang Pradubsuwun, Tomohiro Yoneda, Chris J. Myers. 339-353 [doi]
- Mutation Coverage Estimation for Model CheckingTe-Chang Lee, Pao-Ann Hsiung. 354-368 [doi]
- Modular Model Checking of Software Specifications with Simultaneous Environment GenerationClaudio de la Riva, Javier Tuya. 369-383 [doi]
- Rabin Tree and Its Application to Group Key DistributionHiroaki Kikuchi. 384-391 [doi]
- Using Overlay Networks to Improve VoIP ReliabilityMark J. Karol, P. Krishnan, J. Jenny Li. 392-401 [doi]
- Integrity-Enhanced Verification Scheme for Software-Intensive OrganizationsWen-Kui Chang, Chun-Yuan Chen. 402-414 [doi]
- RCGES: Retargetable Code Generation for Embedded SystemsTrong-Yen Lee, Yang-Hsin Fan, Tsung-Hsun Yang, Chia-Chun Tsai, Wen-Ta Lee, Yuh-Shyan Hwang. 415-425 [doi]
- Verification of Analog and Mixed-Signal Circuits Using Timed Hybrid Petri NetsScott Little, David Walter, Nicholas Seegmiller, Chris J. Myers, Tomohiro Yoneda. 426-440 [doi]
- First-Order LTL Model Checking Using MDGsFang Wang, Sofiène Tahar, Otmane Aït Mohamed. 441-455 [doi]
- Localizing Errors in Counterexample with Iteratively Witness SearchingShengYu Shen, Ying Qin, Sikun Li. 456-469 [doi]
- Verification of WCDMA Protocols and ImplementationAnyi Chen, Jian-Ming Wang, Chiu-Han Hsiao. 470-473 [doi]
- Efficient Representation of Algebraic ExpressionsTsung Lee, Pen-Ho Yu. 474-478 [doi]
- Development of RTOS for PLC Using Formal MethodsJin Hyun Kim, Su-Young Lee, Young Ah Ahn, Jae-Hwan Sim, Jin Seok Yang, Na-Young Lee, Jin-Young Choi. 479-482 [doi]
- Reducing Parametric Automata: A Multimedia Protocol Service Case StudyLin Liu, Jonathan Billington. 483-486 [doi]
- Synthesis of State Feedback Controllers for Parameterized Discrete Event SystemsHans Bherer, Jules Desharnais, Marc Frappier, Richard St.-Denis. 487-490 [doi]
- Solving Box-Pushing Games via Model Checking with OptimizationsGihwon Kwon, Taehoon Lee. 491-494 [doi]
- CLP Based Static Property CheckingTun Li, Yang Guo, Sikun Li. 495-498 [doi]
- A Temporal Assertion Extension to VerilogKai-Hui Chang, Wei-Ting Tu, Yi-Jong Yeh, Sy-Yen Kuo. 499-504 [doi]