Abstract is missing.
- Combining Predicate and Numeric Abstraction for Software Model CheckingArie Gurfinkel, Sagar Chaki. 1-9 [doi]
- Invited Tutorial: Considerations in the Design and Verification of Microprocessors for Safety-Critical and Security-Critical ApplicationsDavid S. Hardin. 1-8 [doi]
- BackSpace: Formal Analysis for Post-Silicon DebugFlavio M. de Paula, Marcel Gort, Alan J. Hu, Steven J. E. Wilton, Jin Yang. 1-10 [doi]
- Formal Verification of Hardware Support for Advanced Encryption StandardAnna Slobodová. 1-4 [doi]
- Trading-Off SAT Search and Variable Quantifications for Effective Unbounded Model CheckingGianpiero Cabodi, Paolo Camurati, Luz Garcia, Marco Murciano, Sergio Nocco, Stefano Quer. 1-8 [doi]
- A Temporal Language for SystemCDeian Tabakov, Gila Kamhi, Moshe Y. Vardi, Eli Singerman. 1-9 [doi]
- Automatic Generation of Local Repairs for Boolean ProgramsRoopsha Samanta, Jyotirmoy V. Deshmukh, E. Allen Emerson. 1-10 [doi]
- Augmenting a Regular Expression-Based Temporal Logic with Local VariablesCindy Eisner, Dana Fisman. 1-8 [doi]
- A Refinement Approach to Design and Verification of On-Chip Communication ProtocolsPeter Böhm, Tom Melham. 1-8 [doi]
- A Theory-Based Decision Heuristic for DPLL(T)Dan Goldwasser, Ofer Strichman, Shai Fine. 1-8 [doi]
- Scaling Up the Formal Verification of Lustre Programs with SMT-Based TechniquesGeorge Hagen, Cesare Tinelli. 1-9 [doi]
- A Theory of Mutations with Applications to Vacuity, Coverage, and Fault ToleranceOrna Kupferman, Wenchao Li, Sanjit A. Seshia. 1-9 [doi]
- A Write-Based Solver for SAT Modulo the Theory of ArraysMiquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric RodrÃguez-Carbonell, Albert Rubio. 1-8 [doi]
- Model Checking Nash Equilibria in MAD Distributed SystemsFederico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci, Lorenzo Alvisi, Allen Clement, Harry C. Li. 1-8 [doi]
- Machine-Code Verification for Multiple Architectures - An Application of Decompilation into LogicMagnus O. Myreen, Michael J. C. Gordon, Konrad Slind. 1-8 [doi]
- Word-Level Sequential Memory Abstraction for Model CheckingPer Bjesse. 1-9 [doi]
- Beyond Vacuity: Towards the Strongest Passing FormulaHana Chockler, Arie Gurfinkel, Ofer Strichman. 1-8 [doi]
- Going with the Flow: Parameterized Verification Using Message FlowsMurali Talupur, Mark R. Tuttle. 1-8 [doi]
- Automatic Formal Verification of Block Cipher ImplementationsEric Whitman Smith, David L. Dill. 1-7 [doi]
- Mechanized Information Flow Analysis through Inductive AssertionsWarren A. Hunt Jr., Robert Bellarmine Krug, Sandip Ray, William D. Young. 1-4 [doi]
- Verifying an Arbiter CircuitChao Yan, Mark R. Greenstreet. 1-9 [doi]
- Recording Synthesis History for Sequential VerificationAlan Mishchenko, Robert K. Brayton. 1-8 [doi]
- BACH : Bounded ReAchability CHecker for Linear Hybrid AutomataLei Bu, You Li, Linzhang Wang, Xuandong Li. 1-4 [doi]
- Optimal Constraint-Preserving Netlist SimplificationJason Baumgartner, Hari Mony, Adnan Aziz. 1-9 [doi]
- Consistency Checking of All Different Constraints over Bit-Vectors within a SAT SolverArmin Biere, Robert Brummayer. 1-4 [doi]
- Invariant-Strengthened Elimination of Dependent State ElementsMichael L. Case, Alan Mishchenko, Robert K. Brayton, Jason Baumgartner, Hari Mony. 1-9 [doi]
- Symbolic Program Analysis Using Term Rewriting and GeneralizationNishant Sinha. 1-9 [doi]
- Automatic Non-Interference Lemmas for Parameterized Model CheckingJesse D. Bingham. 1-8 [doi]
- Scheduling Optimisations for SPIN to Minimise Buffer Requirements in Synchronous Data FlowPieter H. Hartel, Theo C. Ruys, Marc C. W. Geilen. 1-10 [doi]