Loop invariant symbolic execution for parallel programs

DOI10.1007/978-3-642-27940-9_27MaRDI QIDQ2891433zbMATH OpenOpenAlexFDO

Authors Stephen F. Siegel, Timothy K. Zirkel

Publication date 15 June 2012

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-27940-9_27

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Efficient loop navigation for symbolic execution
• Verifying Concurrent Systems with Symbolic Execution
• Model Checking Software
• Interactive verification of concurrent systems using symbolic execution
• Verifying concurrent systems with symbolic execution. Temporal reasoning is symbolic execution with a little induction.

Cites work

• Collective assertions
• Computer aided verification. 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings
• Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences
• scientific article; zbMATH DE number 3538786 (Why is no real title available?)
• scientific article; zbMATH DE number 1956607 (Why is no real title available?)
• Model Checking Software
• Symbolic execution and program testing
• TASS: the toolkit for accurate scientific software
• Tools and Algorithms for the Construction and Analysis of Systems
• Translation validation of loop optimizations and software pipelining in the TVOC framework. In memory of Amir Pnueli

Cited in

(4)

• Collective assertions
• Efficient loop navigation for symbolic execution
• Symbolic Loop Bound Computation for WCET Analysis
• Parallel assertions for architectures with weak memory models

Describes a project that uses

Uses Software

• Corral
• TASS_
• VCC
• Java PathFinder
• KLEE

This page was built for publication: Loop invariant symbolic execution for parallel programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2891433)