We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: F-IDEs with Features and VCs Designed to Assist Human Reasoning When Verification Fails

Authors: Yu-Shan Sun (Clemson University), Daniel Welch (Pennsylvania State University), Murali Sitaraman (Clemson University)
Abstract: This paper summarizes our efforts to aid human reasoning when verification fails through the use of two distinct Formalization Integrated Development Environments (F-IDEs) that we have developed. Both environments are modular and facilitate reasoning about the full behavior of object-based code. The first environment, referred to as the web-IDE, has been used for several years to teach aspects of formal specification and verification, including why and where verification conditions (VCs) arise and how to use them when verification fails. The second F-IDE, RESOLVE Studio, remains experimental, but is a more fully-fledged environment backed by a sequent-based VC generator that produces VCs with fewer extraneous givens. While the environments and VC generation techniques are necessarily language specific, the principles of alternative VC generation methods, F-IDE features, and observations about their impact on novices and experienced users are more generally applicable.
Comments: In Proceedings AppFM 2021, arXiv:2111.07538
Subjects: Logic in Computer Science (cs.LO); Software Engineering (cs.SE)
Journal reference: EPTCS 349, 2021, pp. 51-67
DOI: 10.4204/EPTCS.349.4
Cite as: arXiv:2111.08207 [cs.LO]
  (or arXiv:2111.08207v1 [cs.LO] for this version)

Submission history

From: EPTCS [view email]
[v1] Tue, 16 Nov 2021 03:10:39 GMT (1449kb,D)

Link back to: arXiv, form interface, contact.