Mixed symbolic representations for model checking software programs

No abstract is available for this paper.

• Publication year

  2006

• Venue

  Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2006. MEMOCODE '06. Proceedings.

• Publication date

  2006-07-27

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1109/MEMCOD.2006.1695896
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• A machine program for theorem-proving

  2011influential reference
• Disjunctive image computation for software verification

  2007cited by this paper
• Disjunctive Image Computation for Embedded Software Verification

  2006influential reference
• Model Checking Linear Programs with Arrays

  2006cited by this paper
• Bounded model checking of software using SMT solvers instead of SAT solvers

  2006cited by this paper
• Action Language Verifier, Extended

  2005influential reference
• Model checking C programs using F-Soft

  2005influential reference
• Localization and Register Sharing for Predicate Abstraction

  2005cited by this paper
• F-Soft: Software Verification Platform

  2005cited by this paper
• A Tool for Checking ANSI-C Programs

  2004cited by this paper
• Tools and Algorithms for the Construction and Analysis of Systems

  2003cited by this paper
• Action Language Verifier

  2001influential reference
• Bebop: A Symbolic Model Checker for Boolean Programs

  2000cited by this paper
• Approximate Reachability Analysis of Piecewise-Linear Dynamical Systems

  2000cited by this paper
• An Overview of SAL

  2000influential reference
• Model checking programs

  2000cited by this paper
• Model Checking

  1999cited by this paper
• Composite model-checking

  1999cited by this paper
• IBM Research Report Evaluating the E(cid:11)ectiveness of Pointer Alias Analyses

  1999cited by this paper
• Symbolic Model Checking without BDDs

  1999cited by this paper
• SpC: synthesis of pointers in C application of pointer analysis to the behavioral synthesis from C

  1998cited by this paper
• Verification of Real-Time Systems using Linear Relation Analysis

  1997cited by this paper
• Efficient BDD Algorithms for FSM Synthesis and Verification

  1995cited by this paper
• HYTECH: the next generation

  1995cited by this paper
• Symbolic Model Checking

  1993cited by this paper
• Graph-based Algorithm for Boolean Function Manipulation

  1989cited by this paper
• Combining satisability procedures by equality-sharing

  1984cited by this paper
• The Omega Project

  1978cited by this paper

• Model Reduction of Colored Petri Nets Based on Unrelated Transitions

  2025cites this paper
• Constraint-Based Thread-Modular Abstract Interpretation

  2018cites this paper
• Chapter Two - Advances in Software Model Checking

  2018cites this paper
• Modular verification of interrupt-driven software

  2017cites this paper
• Towards University Semester and Examinations Regulations Model Verification

  2016cites this paper
• Quantitative Masking Strength: Quantifying the Power Side-Channel Resistance of Software Code

  2015cites this paper
• QMS: Evaluating the side-channel resistance of masked software from source code

  2014cites this paper
• Accelerating temporal verification of Simulink diagrams using satisfiability modulo theories

  2014cites this paper
• SMT-Based Verification of Software Countermeasures against Side-Channel Attacks

  2014cites this paper
• Trustworthy and Dynamic Mobile Task Scheduling in Data-Intensive Scientific Workflow Environments

  2013cites this paper
• Control Explicit---Data Symbolic Model Checking: An Introduction

  2013cites this paper
• Constructing Software Structure Graph through Progressive Execution

  2013influential citation
• Efficient state space exploration: Interleaving stateless and state-based model checking

  2010cites this paper
• Action Language verifier: an infinite-state model checker for reactive software specifications

  2009cites this paper
• Software model checking

  2009cites this paper
• Model checking sequential software programs via mixed symbolic analysis

  2009cites this paper
• Bang for the buck: Improvising and scheduling verification engines for effective resource utilization

  2009influential citation
• Dynamic Path Reduction for Software Model Checking

  2009cites this paper
• Efficient SAT-based bounded model checking for software verification

  2008cites this paper
• Modular verification of web services using efficient symbolic encoding and summarization

  2008cites this paper
• Buffer Overflow Detection using Environment Refinement

  2008cites this paper
• Itinerary-Based Access Control for Mobile Tasks in Scientific Workflows

  2007cites this paper
• Induction in CEGAR for Detecting Counterexamples

  2007cites this paper
• Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra

  2007influential citation