demonstration

A HIP and SLEEK verification system

Authors:

OOPSLA '11: Proceedings of the ACM international conference companion on Object oriented programming systems languages and applications companion

Pages 9 - 10

https://doi.org/10.1145/2048147.2048152

Published: 22 October 2011 Publication History

Get Access

Abstract

The HIP and SLEEK systems are aimed at automatic verification of functional correctness of heap manipulating programs. HIP is a separation logic based automated verification system for a simple imperative language, able to modularly verify the specifications of heap-manipulating programs. The specification language allows user defined inductive predicates used to model complex data structures. Specifications can contain both heap constraints and various pure constraints like arithmetic constraints, bag constraints. Based on given annotations for each method/loop, HIP will construct a set of separation logic proof obligations in the form of formula implications which are sent to the SLEEK separation logic prover. SLEEK is a fully automatic prover for separation logic with frame inferring capability.

References

[1]

Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, and Shengchao Qin. Automated verification of shape, size and bag properties. In ICECCS, pages 307--320, 2007.

Digital Library

Google Scholar

[2]

Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, and Shengchao Qin. Multiple pre/post specifications for heap-manipulating methods. In HASE, pages 357--364, 2007.

Digital Library

Google Scholar

[3]

Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, and Shengchao Qin. Enhancing modular oo verification with separation logic. In POPL, pages 87--99, 2008.

Digital Library

Google Scholar

[4]

Cristina David, Cristian Gherghina, and Wei-Ngan Chin. Translation and optimization for a core calculus with exceptions. In PEPM, pages 41--50, 2009.

Digital Library

Google Scholar

[5]

Cristian Gherghina, Cristina David, Shengchao Qin, and Wei-Ngan Chin. Structured specifications for better verification of heap-manipulating programs. In FM, 2011.

Digital Library

Google Scholar

[6]

H. H. Nguyen, C. David, S. C. Qin, and W. N. Chin. Automated Verification of Shape And Size Properties via Separation Logic. In VMCAI, Nice, France, January 2007.

Digital Library

Google Scholar

[7]

Huu Hai Nguyen and Wei-Ngan Chin. Enhancing program verification with lemmas. In CAV, pages 355--369, 2008.

Digital Library

Google Scholar

Cited By

View all

Song YFoo DChin W(2024)Specification and Verification for Unrestricted Algebraic Effects and HandlingProceedings of the ACM on Programming Languages10.1145/36746568:ICFP(909-937)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674656
Lemerre MRival XNicole OIllous H(2024)Advanced Memory and Shape AnalysesGuide to Software Verification with Frama-C10.1007/978-3-031-55608-1_11(487-520)Online publication date: 10-Jul-2024
https://doi.org/10.1007/978-3-031-55608-1_11
Jin ZZhang BCao TCao YWang H(2022)Reasoning about block-based cloud storage systems via separation logicTheoretical Computer Science10.1016/j.tcs.2022.09.015936(43-76)Online publication date: Nov-2022
https://doi.org/10.1016/j.tcs.2022.09.015
Show More Cited By

Index Terms

A HIP and SLEEK verification system
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

Automated verification of the FreeRTOS scheduler in Hip/Sleek

Automated verification of operating system kernels is a challenging problem, partly due to the use of shared mutable data structures. In this paper, we show how we can automatically verify memory safety and functional correctness properties of the task ...
Automated Verification of the FreeRTOS Scheduler in HIP/SLEEK
TASE '12: Proceedings of the 2012 Sixth International Symposium on Theoretical Aspects of Software Engineering

Automated verification of operating system kernels is a challenging problem, partly due to the use of shared mutable data structures. In this paper, we show how we can automatically verify memory safety and functional correctness of the task scheduler ...
Completeness and expressiveness of pointer program verification by separation logic
Abstract
Reynolds' separation logical system for pointer program verification is investigated. This paper proves its completeness theorem that states that every true asserted program is provable in the logical system. In order to prove the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

OOPSLA '11: Proceedings of the ACM international conference companion on Object oriented programming systems languages and applications companion

October 2011

360 pages

ISBN:9781450309424

DOI:10.1145/2048147

General Chair:
Cristina Videira Lopes
University of California, Irvine, USA
,
Program Chair:
Kathleen Fisher
Tufts University, USA

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 October 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Demonstration

Conference

SPLASH '11

Sponsor:

SIGPLAN

SPLASH '11: Conference on Systems, Programming, and Applications: Software for Humanity

October 22 - 27, 2011

Oregon, Portland, USA

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
162
Total Downloads

Downloads (Last 12 months)24
Downloads (Last 6 weeks)7

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Song YFoo DChin W(2024)Specification and Verification for Unrestricted Algebraic Effects and HandlingProceedings of the ACM on Programming Languages10.1145/36746568:ICFP(909-937)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674656
Lemerre MRival XNicole OIllous H(2024)Advanced Memory and Shape AnalysesGuide to Software Verification with Frama-C10.1007/978-3-031-55608-1_11(487-520)Online publication date: 10-Jul-2024
https://doi.org/10.1007/978-3-031-55608-1_11
Jin ZZhang BCao TCao YWang H(2022)Reasoning about block-based cloud storage systems via separation logicTheoretical Computer Science10.1016/j.tcs.2022.09.015936(43-76)Online publication date: Nov-2022
https://doi.org/10.1016/j.tcs.2022.09.015
Watanabe YGopinathan KPîrlea GPolikarpova NSergey I(2021)Certifying the synthesis of heap-manipulating programsProceedings of the ACM on Programming Languages10.1145/34735895:ICFP(1-29)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473589
Polikarpova NSergey I(2019)Structuring the synthesis of heap-manipulating programsProceedings of the ACM on Programming Languages10.1145/32903853:POPL(1-30)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290385
Qin SHe GChin WCraciun FHe MMing Z(2017)Automated specification inference in a combined domain via user-defined predicatesScience of Computer Programming10.1016/j.scico.2017.05.007148:C(189-212)Online publication date: 15-Nov-2017
https://dl.acm.org/doi/10.1016/j.scico.2017.05.007
Le XLo DApel SKhurshid S(2016)Towards efficient and effective automatic program repairProceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering10.1145/2970276.2975934(876-879)Online publication date: 25-Aug-2016
https://dl.acm.org/doi/10.1145/2970276.2975934
Craciun FKiss TCostea A(2015)Towards a Session Logic for Communication ProtocolsProceedings of the 2015 20th International Conference on Engineering of Complex Computer Systems (ICECCS)10.1109/ICECCS.2015.33(140-149)Online publication date: 9-Dec-2015
https://dl.acm.org/doi/10.1109/ICECCS.2015.33
Sharma A(2014)Verified Subtyping with Traits and MixinsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.156.8156(45-51)Online publication date: 8-Jul-2014
https://doi.org/10.4204/EPTCS.156.8
Hofmann M(2013)Ten years of amortized resource analysisProceedings of the 16th international conference on Foundations of Software Science and Computation Structures10.5555/2450348.2450350(xvii-xix)Online publication date: 16-Mar-2013
https://dl.acm.org/doi/10.5555/2450348.2450350
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Automated verification of the FreeRTOS scheduler in Hip/Sleek

Automated Verification of the FreeRTOS Scheduler in HIP/SLEEK

Completeness and expressiveness of pointer program verification by separation logic