Regression-free synthesis for concurrency
Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. 2014. Regression-free synthesis for concurrency. CAV: Computer Aided Verification, LNCS, vol. 8559, 568–584.
Download
IST-2014-297-v1+1_cav14-final.pdf
416.73 KB
[Submitted Version]
IST-2014-297-v2+1_cav14-final2.pdf
616.29 KB
Download (ext.)
https://link.springer.com/chapter/10.1007%2F978-3-319-08867-9_38
[Submitted Version]
Conference Paper
| Published
| English
Scopus indexed
Author
Cerny, Pavol;
Henzinger, Thomas AISTA ;
Radhakrishna, ArjunISTA;
Ryzhyk, Leonid;
Tarrach, ThorstenISTA
Department
Series Title
LNCS
Abstract
While fixing concurrency bugs, program repair algorithms may introduce new concurrency bugs. We present an algorithm that avoids such regressions. The solution space is given by a set of program transformations we consider in the repair process. These include reordering of instructions within a thread and inserting atomic sections. The new algorithm learns a constraint on the space of candidate solutions, from both positive examples (error-free traces) and counterexamples (error traces). From each counterexample, the algorithm learns a constraint necessary to remove the errors. From each positive examples, it learns a constraint that is necessary in order to prevent the repair from turning the trace into an error trace. We implemented the algorithm and evaluated it on simplified Linux device drivers with known bugs.
Publishing Year
Date Published
2014-07-22
Publisher
Springer
Volume
8559
Page
568 - 584
Conference
CAV: Computer Aided Verification
Conference Location
Vienna, Austria
Conference Date
2014-07-18 – 2014-07-22
ISBN
IST-REx-ID
Cite this
Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. Regression-free synthesis for concurrency. In: Vol 8559. Springer; 2014:568-584. doi:10.1007/978-3-319-08867-9_38
Cerny, P., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., & Tarrach, T. (2014). Regression-free synthesis for concurrency (Vol. 8559, pp. 568–584). Presented at the CAV: Computer Aided Verification, Vienna, Austria: Springer. https://doi.org/10.1007/978-3-319-08867-9_38
Cerny, Pavol, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, and Thorsten Tarrach. “Regression-Free Synthesis for Concurrency,” 8559:568–84. Springer, 2014. https://doi.org/10.1007/978-3-319-08867-9_38.
P. Cerny, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, and T. Tarrach, “Regression-free synthesis for concurrency,” presented at the CAV: Computer Aided Verification, Vienna, Austria, 2014, vol. 8559, pp. 568–584.
Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. 2014. Regression-free synthesis for concurrency. CAV: Computer Aided Verification, LNCS, vol. 8559, 568–584.
Cerny, Pavol, et al. Regression-Free Synthesis for Concurrency. Vol. 8559, Springer, 2014, pp. 568–84, doi:10.1007/978-3-319-08867-9_38.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]
Main File(s)
File Name
IST-2014-297-v1+1_cav14-final.pdf
416.73 KB
Access Level
Open Access
Date Uploaded
2018-12-12
MD5 Checksum
a631d3105509f239724644e77a1212e2
File Name
IST-2014-297-v2+1_cav14-final2.pdf
616.29 KB
Access Level
Open Access
Date Uploaded
2018-12-12
MD5 Checksum
f8b0f748cc9fa697ca992cc56c87bc4e
Link(s) to Main File(s)
Access Level
Open Access
Material in ISTA:
Dissertation containing ISTA record