NDLI: Engineering Hoare Logic-Based Program Verification in K Framework

Content Provider	IEEE Xplore Digital Library
Author	Arusoaie, A.
Copyright Year	2013
Description	Author affiliation: Fac. of Comput. Sci., Univ. of Alexandru Ioan Cuza, Iaşi, Romania (Arusoaie, A.)
Abstract	In this paper we describe a methodology for easy development of Hoare Logic verification tools using the K (operational) semantics of programming languages. We exploit the relationship between the Hoare Logic and Matching Logic Reachability, which allows us to translate Hoare triples into reachability rules. Then we use the symbolic execution support to check the derived reachability rules. A Hoare triple holds w.r.t. the partial correctness if and only if the execution of its reachability rule is successful. The methodology consists in enriching the operational semantics of a programming language with syntax and semantics for additional constructs required when using Hoare Logic. The obtained semantics is then used by the K Framework to verify annotated programs. We instantiate our methodology on a simple imperative language, by describing each step separately, and then we test the obtained tool over the KeY-Hoare tests suite.
Starting Page	177
Ending Page	184
File Size	308214
Page Count	8
File Format	PDF
ISBN	9781479930357
e-ISBN	9781479930364
DOI	10.1109/SYNASC.2013.31
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2013-09-23
Publisher Place	Romania
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	hoare logic Computer languages program verification Semantics K framework Transforms Syntactics symbolic execution Educational institutions Concrete Cognition
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Path Directed Symbolic Execution in the K Framework

A Generic Framework for Symbolic Execution:Theory and Applications

Matching logic: a new program verification approach (NIER track)

Soundness of a Logic-Based Verification Method for Imperative Loops

Specifying Languages and Verifying Programs with K

Formalization of the general rules of the Hoare logic using S-formulas

One-Path Reachability Logic

A Generic Framework for Symbolic Execution: Theory and Applications

Forward with hoare [draft dated july 12, 2010].

Engineering Hoare Logic-Based Program Verification in K Framework

Similar Documents

Path Directed Symbolic Execution in the K Framework

A Generic Framework for Symbolic Execution:Theory and Applications

Matching logic: a new program verification approach (NIER track)

Soundness of a Logic-Based Verification Method for Imperative Loops

Specifying Languages and Verifying Programs with K

Formalization of the general rules of the Hoare logic using S-formulas

One-Path Reachability Logic

A Generic Framework for Symbolic Execution: Theory and Applications

Forward with hoare [draft dated july 12, 2010].

Engineering Hoare Logic-Based Program Verification in K Framework