Abstract is missing.
- Rob Tristan Gerth: 1956?2003John O Leary, Marly Roncken. 1-14 [doi]
- Static Program Analysis via 3-Valued LogicThomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm. 15-30 [doi]
- Deductive Verification of Pipelined Machines Using First-Order QuantificationSandip Ray, Warren A. Hunt Jr.. 31-43 [doi]
- A Formal Reduction for Lock-Free Parallel AlgorithmsHui Gao, Wim H. Hesselink. 44-56 [doi]
- An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model CheckingKedar S. Namjoshi. 57-69 [doi]
- Termination of Linear ProgramsAshish Tiwari. 70-82 [doi]
- Symbolic Model Checking of Non-regular PropertiesMartin Lange. 83-95 [doi]
- Proving More Properties with Bounded Model CheckingMohammad Awedh, Fabio Somenzi. 96-108 [doi]
- Parallel LTL-X Model Checking of High-Level Petri Nets Based on UnfoldingsClaus Schröter, Victor Khomenko. 109-121 [doi]
- Using Interface Refinement to Integrate Formal Verification into the Design CycleJacob Chang, Sergey Berezin, David L. Dill. 122-134 [doi]
- Indexed Predicate Discovery for Unbounded System VerificationShuvendu K. Lahiri, Randal E. Bryant. 135-147 [doi]
- Range Allocation for Separation LogicMuralidhar Talupur, Nishant Sinha, Ofer Strichman, Amir Pnueli. 148-161 [doi]
- An Experimental Evaluation of Ground Decision ProceduresLeonardo Mendonça de Moura, Harald Rueß. 162-174 [doi]
- DPLL( T): Fast Decision ProceduresHarald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli. 175-188 [doi]
- Verifying omega-Regular Properties of Markov ChainsDoron Bustan, Sasha Rubin, Moshe Y. Vardi. 189-201 [doi]
- Statistical Model Checking of Black-Box Probabilistic SystemsKoushik Sen, Mahesh Viswanathan, Gul Agha. 202-215 [doi]
- Compositional Specification and Model Checking in GSTEJin Yang, Carl-Johan H. Seger. 216-228 [doi]
- GSTE Is Partitioned Model CheckingRoberto Sebastiani, Eli Singerman, Stefano Tonetta, Moshe Y. Vardi. 229-241 [doi]
- Stuck-Free ConformanceCédric Fournet, C. A. R. Hoare, Sriram K. Rajamani, Jakob Rehof. 242-254 [doi]
- Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional VectorsAmit Goel, Randal E. Bryant. 255-267 [doi]
- Functional Dependency for Verification ReductionJie-Hong Roland Jiang, Robert K. Brayton. 268-280 [doi]
- Verification via Structure SimulationNeil Immerman, Alexander Moshe Rabinovich, Thomas W. Reps, Shmuel Sagiv, Greta Yorsh. 281-294 [doi]
- Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-StructuresFarn Wang. 295-307 [doi]
- Abstraction-Based Satisfiability Solving of Presburger ArithmeticDaniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman. 308-320 [doi]
- Widening Arithmetic AutomataConstantinos Bartzis, Tevfik Bultan. 321-333 [doi]
- Why Model Checking Can Improve WCET AnalysisAlexander Metzner. 334-347 [doi]
- Regular Model Checking for LTL(MSO)Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, Julien d Orso, Mayank Saksena. 348-360 [doi]
- Image Computation in Infinite State Model CheckingAlain Finkel, Jérôme Leroux. 361-371 [doi]
- Abstract Regular Model CheckingAhmed Bouajjani, Peter Habermehl, Tomás Vojnar. 372-386 [doi]
- Global Model-Checking of Infinite-State SystemsNir Piterman, Moshe Y. Vardi. 387-400 [doi]
- QB or Not QB: An Efficient Execution Verification Tool for Memory OrderingsGanesh Gopalakrishnan, Yue Yang, Hemanthkumar Sivaraj. 401-413 [doi]
- Verification of an Advanced mips-Type Out-of-Order Execution AlgorithmTamarah Arons. 414-426 [doi]
- Automatic Verification of Sequential Consistency for Unbounded Addresses and Data ValuesJesse D. Bingham, Anne Condon, Alan J. Hu, Shaz Qadeer, Zhichuan Zhang. 427-439 [doi]
- Efficient Modeling of Embedded Memories in Bounded Model CheckingMalay K. Ganai, Aarti Gupta, Pranav Ashar. 440-452 [doi]
- Understanding Counterexamples with explainAlex Groce, Daniel Kroening, Flavio Lerda. 453-456 [doi]
- Zapato: Automatic Theorem Proving for Predicate Abstraction RefinementThomas Ball, Byron Cook, Shuvendu K. Lahiri, Lintao Zhang. 457-461 [doi]
- JNuke: Efficient Dynamic Analysis for JavaCyrille Artho, Viktor Schuppan, Armin Biere, Pascal Eugster, Marcel Baur, Boris Zweimüller. 462-465 [doi]
- The HiVy Tool SetPaula J. Pingree, Erich Mikk. 466-469 [doi]
- ObsSlice: A Timed Automata Slicer Based on ObserversVíctor A. Braberman, Diego Garbervetsky, Alfredo Olivero. 470-474 [doi]
- The UCLID Decision ProcedureShuvendu K. Lahiri, Sanjit A. Seshia. 475-478 [doi]
- MCK: Model Checking the Logic of KnowledgePeter Gammie, Ron van der Meyden. 479-483 [doi]
- Zing: A Model Checker for Concurrent SoftwareTony Andrews, Shaz Qadeer, Sriram K. Rajamani, Jakob Rehof, Yichen Xie. 484-487 [doi]
- The Mec 5 Model-CheckerAlain Griffault, Aymeric Vincent. 488-491 [doi]
- PlayGame: A Platform for Diagnostic GamesLi Tan. 492-495 [doi]
- SAL 2Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar, Maria Sorea, Ashish Tiwari. 496-500 [doi]
- Formal Analysis of Java Programs in JavaFANAzadeh Farzan, Feng Chen, José Meseguer, Grigore Rosu. 501-505 [doi]
- A Toolset for Modelling and Verification of GALS SystemsS. Ramesh, Sampada Sonalkar, Vijay D Silva, Naveen Chandra, B. Vijayalakshmi. 506-509 [doi]
- WSAT: A Tool for Formal Analysis of Web ServicesXiang Fu, Tevfik Bultan, Jianwen Su. 510-514 [doi]
- CVC Lite: A New Implementation of the Cooperating Validity Checker Category BClark W. Barrett, Sergey Berezin. 515-518 [doi]
- CirCUs: A Satisfiability Solver Geared towards Bounded Model CheckingHoonSang Jin, Mohammad Awedh, Fabio Somenzi. 519-522 [doi]
- Mechanical Mathematical Methods for Microprocessor VerificationWarren A. Hunt Jr.. 523-533 [doi]