Combining static concurrency analysis with symbolic execution
- 1 October 1988
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. 14 (10) , 1499-1511
- https://doi.org/10.1109/32.6195
Abstract
Static concurrency analysis detects anomalous synchronization patterns in concurrent programs, but may also report spurious errors involving infeasible execution paths. Integrated application of static concurrency analysis and symbolic execution sharpens the results of the former without incurring the full costs of the latter when applied in isolation. Concurrency analysis acts as a path selection mechanism for symbolic execution, while symbolic execution acts as a pruning mechanism for concurrency analysis. Methods of combining the techniques follow naturally from explicit characterization and comparison of the state spaces explored by each, suggesting a general approach for integrating state-based program analysis techniques in a software development environment.Keywords
This publication has 18 references indexed in Scilit:
- How to leave out details: error-preserving abstractions of state-space modelsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Interactive State-Space Analysis of Concurrent SystemsIEEE Transactions on Software Engineering, 1987
- Next Generation Software Environments: Principles, Problems, and Research DirectionsPublished by Defense Technical Information Center (DTIC) ,1987
- Automated Protocol Validation in Argos: Assertion Proving and Scatter SearchingIEEE Transactions on Software Engineering, 1987
- Constrained expressions: Adding analysis capabilities to design methods for concurrent software systemsIEEE Transactions on Software Engineering, 1986
- Modeling the Ada task system by Petri netsComputer Languages, 1985
- Complexity of analyzing the synchronization structure of concurrent programsActa Informatica, 1983
- Communicating sequential processesCommunications of the ACM, 1978
- HAL/S - The Avionics Programming System for ShuttlePublished by American Institute of Aeronautics and Astronautics (AIAA) ,1977
- An Introduction to Proving the Correctness of ProgramsACM Computing Surveys, 1976