publication . Conference object . 2015

Sliced Path Prefixes: An Effective Method to Enable Refinement Selection

Beyer , Dirk; Löwe , Stefan; Wendler , Philipp;
Open Access English
  • Published: 02 Jun 2015
  • Publisher: Springer International Publishing
Abstract
Part 5: Efficient Verification Techniques; International audience; Automatic software verification relies on constructing, for a given program, an abstract model that is (1) abstract enough to avoid state-space explosion and (2) precise enough to reason about the specification. Counterexample-guided abstraction refinement is a standard technique that suggests to extract information from infeasible error paths, in order to refine the abstract model if it is too imprecise. Existing approaches —including our previous work— do not choose the refinement for a given path systematically. We present a method that generates alternative refinements and allows to systemati...
Subjects
free text keywords: [ INFO.INFO-NI ] Computer Science [cs]/Networking and Internet Architecture [cs.NI], Constraint Sequence, Abstract Model, [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], Interpolation Problem, [INFO]Computer Science [cs], [ INFO ] Computer Science [cs], Abstract Domain, Program Location
22 references, page 1 of 2

1. A. Albarghouthi, Y. Li, A. Gurfinkel, and M. Chechik. Ufo: A framework for abstraction- and interpolation-based software verification. In Proc. CAV, LNCS 7358, pages 672-678. Springer, 2012.

2. F. Alberti, R. Bruttomesso, S. Ghilardi, S. Ranise, and N. Sharygina. An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods in System Design, 45(1):63-109, 2014.

3. S. Apel, D. Beyer, K. Friedberger, F. Raimondi, and A. von Rhein. Domain types: Abstract-domain selection based on variable usage. In Proc. HVC, LNCS 8244, pages 262-278. Springer, 2013.

4. T. Ball, B. Cook, V. Levin, and S.K. Rajamani. SLAM and Static Driver Verifier: Technology transfer of formal methods inside Microsoft. In Proc. IFM, LNCS 2999, pages 1-20. Springer, 2004.

5. T. Ball and S. K. Rajamani. The Slam project: Debugging system software via static analysis. In Proc. POPL, pages 1-3. ACM, 2002.

6. D. Beyer. Software verification and verifiable witnesses (Report on SV-COMP 2015). In Proc. TACAS, LNCS 9035, pages 401-416. Springer, 2015.

7. D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar. The software model checker Blast. Int. J. Softw. Tools Technol. Transfer, 9(5-6):505-525, 2007.

8. D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko. Path invariants. In Proc. PLDI, pages 300-309. ACM, 2007. [OpenAIRE]

9. D. Beyer, T. A. Henzinger, and G. Théoduloz. Program analysis with dynamic precision adjustment. In Proc. ASE, pages 29-38. IEEE, 2008. [OpenAIRE]

10. D. Beyer and M. E. Keremoglu. CPAchecker: A tool for configurable software verification. In Proc. CAV, LNCS 6806, pages 184-190. Springer, 2011.

11. D. Beyer and S. Löwe. Explicit-state software model checking based on CEGAR and interpolation. In Proc. FASE, LNCS 7793, pages 146-162. Springer, 2013.

12. D. Beyer, S. Löwe, and P. Wendler. Domain-type-guided refinement selection based on sliced path prefixes. Technical Report MIP-1501, University of Passau, January 2015. arXiv:1502.00045.

13. D. Beyer and A. K. Petrenko. Linux driver verification. In Proc. ISoLA, LNCS 7610, pages 1-6. Springer, 2012.

14. B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. In Proc. PLDI, pages 196-207. ACM, 2003.

15. E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM, 50(5):752-794, 2003.

22 references, page 1 of 2
Abstract
Part 5: Efficient Verification Techniques; International audience; Automatic software verification relies on constructing, for a given program, an abstract model that is (1) abstract enough to avoid state-space explosion and (2) precise enough to reason about the specification. Counterexample-guided abstraction refinement is a standard technique that suggests to extract information from infeasible error paths, in order to refine the abstract model if it is too imprecise. Existing approaches —including our previous work— do not choose the refinement for a given path systematically. We present a method that generates alternative refinements and allows to systemati...
Subjects
free text keywords: [ INFO.INFO-NI ] Computer Science [cs]/Networking and Internet Architecture [cs.NI], Constraint Sequence, Abstract Model, [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], Interpolation Problem, [INFO]Computer Science [cs], [ INFO ] Computer Science [cs], Abstract Domain, Program Location
22 references, page 1 of 2

1. A. Albarghouthi, Y. Li, A. Gurfinkel, and M. Chechik. Ufo: A framework for abstraction- and interpolation-based software verification. In Proc. CAV, LNCS 7358, pages 672-678. Springer, 2012.

2. F. Alberti, R. Bruttomesso, S. Ghilardi, S. Ranise, and N. Sharygina. An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods in System Design, 45(1):63-109, 2014.

3. S. Apel, D. Beyer, K. Friedberger, F. Raimondi, and A. von Rhein. Domain types: Abstract-domain selection based on variable usage. In Proc. HVC, LNCS 8244, pages 262-278. Springer, 2013.

4. T. Ball, B. Cook, V. Levin, and S.K. Rajamani. SLAM and Static Driver Verifier: Technology transfer of formal methods inside Microsoft. In Proc. IFM, LNCS 2999, pages 1-20. Springer, 2004.

5. T. Ball and S. K. Rajamani. The Slam project: Debugging system software via static analysis. In Proc. POPL, pages 1-3. ACM, 2002.

6. D. Beyer. Software verification and verifiable witnesses (Report on SV-COMP 2015). In Proc. TACAS, LNCS 9035, pages 401-416. Springer, 2015.

7. D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar. The software model checker Blast. Int. J. Softw. Tools Technol. Transfer, 9(5-6):505-525, 2007.

8. D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko. Path invariants. In Proc. PLDI, pages 300-309. ACM, 2007. [OpenAIRE]

9. D. Beyer, T. A. Henzinger, and G. Théoduloz. Program analysis with dynamic precision adjustment. In Proc. ASE, pages 29-38. IEEE, 2008. [OpenAIRE]

10. D. Beyer and M. E. Keremoglu. CPAchecker: A tool for configurable software verification. In Proc. CAV, LNCS 6806, pages 184-190. Springer, 2011.

11. D. Beyer and S. Löwe. Explicit-state software model checking based on CEGAR and interpolation. In Proc. FASE, LNCS 7793, pages 146-162. Springer, 2013.

12. D. Beyer, S. Löwe, and P. Wendler. Domain-type-guided refinement selection based on sliced path prefixes. Technical Report MIP-1501, University of Passau, January 2015. arXiv:1502.00045.

13. D. Beyer and A. K. Petrenko. Linux driver verification. In Proc. ISoLA, LNCS 7610, pages 1-6. Springer, 2012.

14. B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. In Proc. PLDI, pages 196-207. ACM, 2003.

15. E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM, 50(5):752-794, 2003.

22 references, page 1 of 2
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue
publication . Conference object . 2015

Sliced Path Prefixes: An Effective Method to Enable Refinement Selection

Beyer , Dirk; Löwe , Stefan; Wendler , Philipp;