Proving Correctness of an Efficient Abstraction for Interrupt Handling

No abstract is available for this paper.

• Publication year

  2008

• Venue

  International Workshop on Systems Software Verification

• Publication date

  2008-07-01

• Fields of study

  Computer Science, Engineering

• Identifiers
  DOI 10.1016/j.entcs.2008.06.046
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Model checking of software for microcontrollers

  2010cited by this paper
• Model checking C source code for embedded systems

  2009cited by this paper
• Delayed Nondeterminism in Model Checking Embedded Systems Assembly Code

  2007influential reference
• Applying Model Checking to an Automotive Microcontroller Application

  2007cited by this paper
• Application of Static Analyses for State Space Reduction to Microcontroller Assembly Code

  2007cited by this paper
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols

  2007cited by this paper
• Challenges and Applications of Assembly-Level Software Model Checking

  2006cited by this paper
• [mc]square: A Model Checker for Microcontroller Code

  2006cited by this paper
• Model Checking Machine Code with the GNU Debugger

  2005influential reference
• DART: directed automated random testing

  2005cited by this paper
• WYSINWYX: What you see is not what you eXecute

  2005cited by this paper
• CUTE: a concolic unit testing engine for C

  2005cited by this paper
• Directed Error Detection in C++ with the Assembly-Level Model Checker StEAM

  2004influential reference
• The SPIN Model Checker - primer and reference manual

  2003influential reference
• Model checking programs

  2000cited by this paper
• Model Checking the Branching Time Temporal Logic CTL

  1997cited by this paper
• Uppaal in a nutshell

  1997influential reference
• A lazy non-deterministic functional language.

  1995cited by this paper
• A natural semantics for lazy evaluation

  1993cited by this paper
• A Linear Local Model Checking Algorithm for CTL

  1993cited by this paper
• Temporal and Modal Logic

  1991cited by this paper
• Handbook of theoretical computer science - Part A: Algorithms and complexity; Part B: Formal models and semantics

  1990cited by this paper
• A methodology for hardware verification based on logic simulation

  1987cited by this paper

• Model checking of software for microcontrollers

  2010cites this paper
• Deliverable no . : D 2 . 3 Title of Deliverable : Abstraction

  2010cites this paper
• Deliverable no . : D 2 . 3 Title of Deliverable : Abstraction

  2010cites this paper
• Model checking C source code for embedded systems

  2009cites this paper
• Reduction of Interrupt Handler Executions for Model Checking Embedded Software

  2009cites this paper