Invited Talks

• 
  Gérard Berry: Esterel and Jazz: Two Synchronous Languages for Circuit Design (Abstract). 1
• 
  Peter Jansen: Design Process of Embedded Automotive Systems - Using Model Checking for Correct Specification. 2-7

Proof of Microprocessors

• 
  Ravi Hosabettu, Ganesh Gopalakrishnan, Mandayam K. Srivas: A Proof of Correctness of a Processor Implementing Tomasulo's Algorithm without a Reorder Buffer. 8-22
• 
  Byron Cook, John Launchbury, John Matthews, Richard B. Kieburtz: Formal Verification of Explicitly Parallel Microprocessors. 23-36
• 
  Miroslav N. Velev, Randal E. Bryant: Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic. 37-53

Model Checking

• 
  Yuan Yu, Panagiotis Manolios, Leslie Lamport: Model Checking TLA⁺ Specifications. 54-66
• 
  Nina Amla, E. Allen Emerson, Kedar S. Namjoshi: Efficient Decompositional Model Checking for Regular Timing Diagrams. 67-81
• 
  Orna Kupferman, Moshe Y. Vardi: Vacuity Detection in Temporal Model Checking. 82-96

Formal Methiods and Industrial Applications

• 
  Cindy Eisner: Using Symbolic Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard. 97-109
• 
  Ying Xu, Eduard Cerny, Allan Silburt, A. Coady, Ying Liu, Philip Pownall: Practical Application of Formal Verification Techniques on a Frame Mux/Demux Chip from Nortel Semiconductors. 110-124
• 
  Marius Bozga, Oded Maler, Stavros Tripakis: Efficient Verification of Timed Automata Using Dense and Discrete Time Semantics. 125-141

Abstraction and Compositional Techniques

• 
  E. Allen Emerson, Richard J. Trefler: From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking. 142-156
• 
  Dirk W. Hoffmann, Thomas Kropf: Automatic Error Correction of Large Circuits Using Boolean Decomposition and Abstraction. 157-171
• 
  Edmund M. Clarke, Somesh Jha, Yuan Lu, Dong Wang: Abstract BDDs: A Technque for Using Abstraction in Model Checking. 172-186

Theorem Proving Related Approaches

• 
  Christian Blumenröhr, Viktor K. Sabelfeld: Formal Synthesis at the Algorithmic Level. 187-201
• 
  Mark Aagaard, Thomas F. Melham, John W. O'Leary: Xs are for Trajectory Evaluation, Booleans are for Theorem Proving. 202-218
• 
  Kenneth L. McMillan: Verification of Infinite State Systems by Compositional Model Checking. 219-234

Symbolic Simulation/Symbolic Traversal

• 
  Gerd Ritter, Hans Eveking, Holger Hinrichsen: Formal Verification of Designs with Complex Control by Symbolic Simulation. 234-249
• 
  Kavita Ravi, Fabio Somenzi: Hints to accelerate Symbolic Traversal. 250-264

Specification Languages and Methodologies

• 
  Jürgen Ruf, Thomas Kropf: Modleing and Checking Networks of Communicating Real-Time Process. 265-279
• 
  Sagi Katz, Orna Grumberg, Daniel Geist: "Have I written enough Properties?" - A Method of Comparison between Specification and Implementation. 280-297
• 
  Edmund M. Clarke, Masahiro Fujita, Sreeranga P. Rajan, Thomas W. Reps, Subash Shankar, Tim Teitelbaum: Program Slicing of Hardware Description Languages. 298-312

Posters

• 
  Jun Sawada, Warren A. Hunt Jr.: Results of the Verification of a Complex Pipelined Machine Model. 313-316
• 
  Hüsnü Yenigün, Vladimir Levin, Doron Peled, Peter A. Beerel: Hazard-Freedom Checking in Speed-Independent Systems. 317-320
• 
  Klaus Schneider: Yet another Look at the LTL Model Checking. 321-325
• 
  Stefan Hendricx, Luc J. M. Claesen: Verification of Finite-State-Machine Refinements Using a Symbolic Methodology. 326-329
• 
  George Economakos, George K. Papakonstantinou: Refinement and Property Checking in High-Level Synthesis using Attribute Grammars. 330-333
• 
  Steven D. Johnson, Yanhong A. Liu, Yuchen Zhang: A Systematic Incrementalization Technique and Its Application to Hardware Design. 334-337
• 
  Kathi Fisler, Moshe Y. Vardi: Bisimulation and Model Checking. 338-341
• 
  Kenneth L. McMillan: Circular Compositional Reasoning about Liveness. 342-345
• 
  Nancy A. Day, Jeffrey R. Lewis, Byron Cook: Symbolic Simulation of Microprocessor Models using Type Classes in Haskell. 346-349
• 
  Aarti Gupta, Pranav Ashar, Sharad Malik: Exploiting Retiming in a Guided Simulation Based Validation Methodology. 350-353
• 
  Jens Chr. Godesken: Fault Models for Embedded Systems (Extended Abstract). 354-359
• 
  Klaus Schneider, Michaela Huhn, George Logothetis: Validation of Object-Oriented Concurrent Designs by Model Checking. 360-364

last updated on Thu May 23 03:08:46 2013 by the dblp team
data released under the ODC-BY 1.0 license
see also our legal information page