Using model checking with symbolic execution to verify parallel numerical programs

No abstract is available for this paper.

• Publication year

  2006

• Venue

  International Symposium on Software Testing and Analysis

• Publication date

  2006-07-21

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1145/1146238.1146256
• 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 Nonblocking MPI Programs

  2007cited by this paper
• Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives

  2005cited by this paper
• An Overview of Semantics for the Validation of Numerical Programs

  2005cited by this paper
• VYRD: verifYing concurrent programs by runtime refinement-violation detection

  2005influential reference
• Modeling wildcard-free MPI programs for verification

  2005cited by this paper
• Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings

  2005cited by this paper
• MODELING MPI PROGRAMS FOR VERIFICATION

  2004cited by this paper
• Model checking software : 11th International SPIN Workshop, Barcelona, Spain, April 1-3, 2004 ; proceedings

  2004cited by this paper
• Verification of Java Programs Using Symbolic Execution and Invariant Generation

  2004cited by this paper
• Verification of MPI-Based Software for Scientific Computation

  2004cited by this paper
• The SPIN Model Checker

  2003cited by this paper
• Bogor: an extensible and highly-modular software model checking framework

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

  2003cited by this paper
• Parallel Scientific Computing in C++ and MPI : A Seamless Approach to Parallel Algorithms and their

  2002cited by this paper
• Automatically validating temporal safety properties of interfaces

  2001cited by this paper
• MPI - The Complete Reference: Volume 1, The MPI Core

  1998cited by this paper
• Mpi-2: extensions to the message-passing interface

  1997cited by this paper
• What every computer scientist should know about floating-point arithmetic

  1991cited by this paper
• IEEE Standard for Binary Floating Point Arithmetic

  1985cited by this paper
• A System to Generate Test Data and Symbolically Execute Programs

  1976cited by this paper
• An Introduction to Proving the Correctness of Programs

  1976cited by this paper
• SELECT—a formal system for testing and debugging programs by symbolic execution

  1975cited by this paper
• An introduction to the theory of groups

  1960cited by this paper

• Leveraging LLMs to Automate Energy-Aware Refactoring of Parallel Scientific Codes

  2025cites this paper
• Combining rule- and SMT-based reasoning for verifying floating-point Java programs in KeY

  2023cites this paper
• PEQCHECK: Localized and Context-aware Checking of Functional Equivalence

  2021cites this paper
• Deductive Verification of Floating-Point Java Programs in KeY

  2021cites this paper
• Verification of Functional Correctness of Code Diversification Techniques

  2021cites this paper
• Combining Model Checking and Testing

  2018cites this paper
• Enabling Fast and Accurate Run-Time Decisions in Geo-Distributed Systems: Better Achieving Service Level Objectives

  2018cites this paper
• Verifying Parallel Code After Refactoring Using Equivalence Checking

  2018cites this paper
• The role of model checking in software engineering

  2018cites this paper
• A generic framework for symbolic execution: A coinductive approach

  2017cites this paper
• Nequivack: Assessing Mutation Score Confidence

  2016cites this paper
• A systematic review of approaches for testing concurrent programs

  2016cites this paper
• Reducing Long Tail Latencies in Geo-Distributed Systems

  2016cites this paper
• Calculation coverage testing in scientific applications

  2015cites this paper
• Combining Algebraic and Domain Testing to Design Adequate Test Cases for Signal Processing Algorithms

  2015cites this paper
• The nearest replica can be farther than you think

  2015cites this paper
• Partial Order Reduction for Security Protocols

  2015cites this paper
• Symbolic execution based on language transformation

  2015cites this paper
• Numerical program analysis and testing

  2014cites this paper
• An Algorithm for Static Tracing of Message Passing Interface Programs Using Data Flow Analysis

  2014cites this paper
• Automatic Generation of Valid Parallel-Processes Transition Using Genetic Algorithms and Communication-Flow Analysis

  2014cites this paper
• Symbolic Crosschecking of Data-Parallel Floating-Point Code

  2014cites this paper
• Model Checking Parallel Programs with Inputs

  2014cites this paper
• Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis

  2013cites this paper
• Symbolic crosschecking of data-parallel floating point code

  2013cites this paper
• A domain-specific language and scalable middleware for particle-mesh simulations on heterogeneous parallel computers

  2013cites this paper
• Chapter 10 Par Lab Progress on Correctness Tools for Parallel Programs

  2013cites this paper
• A Generic Framework for Symbolic Execution

  2013cites this paper
• Secure Virtualization with Formal Methods

  2013cites this paper
• Un Verificador de Escenarios Arquitectónicos en Tiempo de Ejecución usando Redes de Petri Coloreadas A Verifier of Runtime Architectural Scenarios using Colored Petri Nets

  2012cites this paper
• Underspecified harnesses and interleaved bugs

  2012cites this paper
• Automated coverage calculation and test case generation

  2012cites this paper
• Green: reducing, reusing and recycling constraints in program analysis

  2012cites this paper
• Active Testing: Predicting and Confirming Concurrency Bugs for Concurrent and Distributed Memory Parallel Systems

  2012cites this paper
• Generating Data Race Witnesses by an SMT-Based Analysis

  2011cites this paper
• The Toolkit for Accurate Scientific Software

  2011cites this paper
• Differencing Labeled Transition Systems

  2011cites this paper
• Scalable Formal Dynamic Verification of MPI Programs Through Distributed Causality Tracking

  2011cites this paper
• Towards Verification of MPJ-based Java Programs

  2011cites this paper
• Contribuições para o Teste de Software

  2011cites this paper
• Symbolic Testing of OpenCL Code

  2011cites this paper
• Symbolic execution with mixed concrete-symbolic solving

  2011cites this paper
• TASS: The Toolkit for Accurate Scientific Software

  2011cites this paper
• Metamorphic testing techniques to detect defects in applications without test oracles

  2010cites this paper
• COMPOSABLE SIMULATION MODELS AND THEIR FORMAL VALIDATION

  2010influential citation
• Sireum/Topi LDP: a lightweight semi-decision procedure for optimizing symbolic execution-based analyses

  2009cites this paper
• A survey of new trends in symbolic execution for software testing and analysis

  2009cites this paper
• Design Validation by Symbolic Simulation and Equivalence Checking: A Case Study in Memory Optimization for Image Manipulation

  2009cites this paper
• A Case Study in Using Formal Methods to Verify Programs That Use MPI One-Sided Communication

  2009cites this paper
• A document driven methodology for developing a high quality Parallel Mesh Generation Toolbox

  2009cites this paper
• Generalized Abstract Symbolic Summaries

  2009cites this paper
• An algebraic specification of message passing programming languages

  2009cites this paper
• MPIWiz: subgroup reproducible replay of mpi applications

  2009cites this paper
• Race directed random testing of concurrent programs

  2008cites this paper
• KOALA: a co-allocating grid scheduler

  2008cites this paper
• Differential symbolic execution

  2008cites this paper
• Randomized active atomicity violation detection in concurrent programs

  2008cites this paper
• Structural testing criteria for message‐passing parallel programs

  2008cites this paper
• Generating Exact Approximations to Model Check Concurrent Systems

  2008cites this paper
• Barrier matching for programs with textually unaligned barriers

  2007cites this paper
• MPI-Model-Checking in C-Programmen

  2007cites this paper
• Formal Methods Applied to HPC Software Design : A Case Study of Locking Based on MPI One-Sided Communication

  2007cites this paper
• Verification of Halting Properties for MPI Programs Using Nonblocking Operations

  2007cites this paper
• Productivity with performance: property/behavior-based automated composition of parallel programs from self-describing components

  2007cites this paper
• A Case Study in the Use of Model Checking to Verify Parallel Scientific Software

  2007cites this paper
• Model Checking Nonblocking MPI Programs

  2007cites this paper
• Effective random testing of concurrent programs

  2007cites this paper
• Concolic Testing of Multithreaded Programs and Its Application to Testing Security Protocols

  2006cites this paper
• A Race-Detection and Flipping Algorithm for Automated Testing of Multi-threaded Programs

  2006cites this paper
• Formal Verification of Programs That Use MPI One-Sided Communication

  2006cites this paper
• Gauss: A Framework for Verifying Scientific Computing Software

  2006cites this paper
• Scalable Automated Methods for Dynamic Program Analysis

  2006cites this paper
• Concolic Testing of Sequential and Concurrent Programs

  2006cites this paper
• Automated Testing of Multithreaded Programs Using Race-Detection and Flipping

  2006cites this paper
• Refactoring SPIN for Safety

  2005influential citation