publication . Preprint . 2017

Scheduling Constraint Based Abstraction Refinement for Multi-Threaded Program Verification

Yin, Liangze; Dong, Wei; Liu, Wanwei; Wang, Ji;
Open Access English
  • Published: 22 Aug 2017
Abstract
Bounded model checking is among the most efficient techniques for the automatic verification of concurrent programs. However, encoding all possible interleavings often requires a huge and complex formula, which significantly limits the salability. This paper proposes a novel and efficient abstraction refinement method for multi-threaded program verification. Observing that the huge formula is usually dominated by the exact encoding of the scheduling constraint, this paper proposes a \tsc based abstraction refinement method, which avoids the huge and complex encoding of BMC. In addition, to obtain an effective refinement, we have devised two graph-based algorithm...
Subjects
free text keywords: Computer Science - Programming Languages
Download from
43 references, page 1 of 3

[1] Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos F. Sagonas. 2014. Optimal dynamic partial order reduction. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL. 373-384. [OpenAIRE]

[2] Sarita V. Adve and Kourosh Gharachorloo. 1996. Shared Memory Consistency Models: A Tutorial. IEEE Computer 29, 12 (1996), 66-76.

[3] Jade Alglave, Daniel Kroening, and Michael Tautschnig. 2013. Partial Orders for Eficient Bounded Model Checking of Concurrent Software. In International Conference on Computer Aided Verification, CAV . 141-157.

[4] Jiri Barnat, Lubos Brim, Vojtech Havel, Jan Havlícek, Jan Kriho, Milan Lenco, Petr Rockai, Vladimír Still, and Jirí Weiser. 2013. DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs. In International Conference on Computer Aided Verification, CAV . 863-868.

[5] Tom Bergan, Luis Ceze, and Dan Grossman. 2013. Input-covering schedules for multithreaded programs. In ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA. 677-692.

[6] Dirk Beyer. 2017. Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2017). In International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS.

[7] Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. 1999. Symbolic Model Checking without BDDs. In International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS. 193-207.

[8] Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. 2015. Tractable Refinement Checking for Concurrent Objects. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL. 651-662. [OpenAIRE]

[9] Katherine E. Coons, Madan Musuvathi, and Kathryn S. McKinley. 2013. Bounded partial-order reduction. In ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA. 833-848.

[10] Lucas C. Cordeiro, Jeremy Morse, Denis Nicole, and Bernd Fischer. 2012. Context-Bounded Model Checking with ESBMC 1.17 - (Competition Contribution). In International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS. 534-537.

[11] Andrei Marian Dan, Yuri Meshman, Martin T. Vechev, and Eran Yahav. 2013. Predicate Abstraction for Relaxed Memory Models. In International Static Analysis Symposium, SAS. 84-104.

[12] Andrei Marian Dan, Yuri Meshman, Martin T. Vechev, and Eran Yahav. 2015. Efective Abstractions for Verification under Relaxed Memory Models. In International Conference on Verification, Model Checking and Abstract Interpretation, VMCAI. 449-466.

[13] Pantazis Deligiannis, Alastair F. Donaldson, and Zvonimir Rakamaric. 2015. Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers (T). In 30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015, Lincoln, NE, USA. 166-177. [OpenAIRE]

[14] Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, and Hongseok Yang. 2013. Views: compositional reasoning for concurrent programs. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL. 287-300.

[15] Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, and Sharon Shoham. 2015. Automated Circular AssumeGuarantee Reasoning. In International Symposium on Formal Methods, FM. 23-39.

43 references, page 1 of 3
Abstract
Bounded model checking is among the most efficient techniques for the automatic verification of concurrent programs. However, encoding all possible interleavings often requires a huge and complex formula, which significantly limits the salability. This paper proposes a novel and efficient abstraction refinement method for multi-threaded program verification. Observing that the huge formula is usually dominated by the exact encoding of the scheduling constraint, this paper proposes a \tsc based abstraction refinement method, which avoids the huge and complex encoding of BMC. In addition, to obtain an effective refinement, we have devised two graph-based algorithm...
Subjects
free text keywords: Computer Science - Programming Languages
Download from
43 references, page 1 of 3

[1] Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos F. Sagonas. 2014. Optimal dynamic partial order reduction. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL. 373-384. [OpenAIRE]

[2] Sarita V. Adve and Kourosh Gharachorloo. 1996. Shared Memory Consistency Models: A Tutorial. IEEE Computer 29, 12 (1996), 66-76.

[3] Jade Alglave, Daniel Kroening, and Michael Tautschnig. 2013. Partial Orders for Eficient Bounded Model Checking of Concurrent Software. In International Conference on Computer Aided Verification, CAV . 141-157.

[4] Jiri Barnat, Lubos Brim, Vojtech Havel, Jan Havlícek, Jan Kriho, Milan Lenco, Petr Rockai, Vladimír Still, and Jirí Weiser. 2013. DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs. In International Conference on Computer Aided Verification, CAV . 863-868.

[5] Tom Bergan, Luis Ceze, and Dan Grossman. 2013. Input-covering schedules for multithreaded programs. In ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA. 677-692.

[6] Dirk Beyer. 2017. Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2017). In International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS.

[7] Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. 1999. Symbolic Model Checking without BDDs. In International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS. 193-207.

[8] Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. 2015. Tractable Refinement Checking for Concurrent Objects. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL. 651-662. [OpenAIRE]

[9] Katherine E. Coons, Madan Musuvathi, and Kathryn S. McKinley. 2013. Bounded partial-order reduction. In ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA. 833-848.

[10] Lucas C. Cordeiro, Jeremy Morse, Denis Nicole, and Bernd Fischer. 2012. Context-Bounded Model Checking with ESBMC 1.17 - (Competition Contribution). In International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS. 534-537.

[11] Andrei Marian Dan, Yuri Meshman, Martin T. Vechev, and Eran Yahav. 2013. Predicate Abstraction for Relaxed Memory Models. In International Static Analysis Symposium, SAS. 84-104.

[12] Andrei Marian Dan, Yuri Meshman, Martin T. Vechev, and Eran Yahav. 2015. Efective Abstractions for Verification under Relaxed Memory Models. In International Conference on Verification, Model Checking and Abstract Interpretation, VMCAI. 449-466.

[13] Pantazis Deligiannis, Alastair F. Donaldson, and Zvonimir Rakamaric. 2015. Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers (T). In 30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015, Lincoln, NE, USA. 166-177. [OpenAIRE]

[14] Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, and Hongseok Yang. 2013. Views: compositional reasoning for concurrent programs. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL. 287-300.

[15] Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, and Sharon Shoham. 2015. Automated Circular AssumeGuarantee Reasoning. In International Symposium on Formal Methods, FM. 23-39.

43 references, page 1 of 3
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue