Using answer set programming in the development of verified software

DOI10.4230/LIPICS.ICLP.2012.72MaRDI QIDQ5398045zbMATH OpenOpenAlexFDO

Authors Florian Schanda, Martin Brain

Publication date 25 February 2014

Full work available at URL https://dblp.uni-trier.de/db/conf/iclp/iclp2012.html#SchandaB12

zbMATH Keywords

Adaanswer set programmingcontract based verificationsafety criticalSPARKverification

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in artificial intelligence (68T27)

Recommendations

• Model Checking Abstract State Machines with Answer Set Programming
• Modular answer set programming as a formal specification language
• Methods and methodologies for developing answer-set programs -- project description
• Verification for ASP denotational semantics: a case study using the PVS theorem prover
• Zap: Automated Theorem Proving for Software Analysis

Cited in

(4)

• Instrumenting a weakest precondition calculus for counterexample generation
• An automatically verified prototype of the Tokeneer ID station specification
• Are the logical foundations of verifying compiler prototypes matching user expectations?
• Formal software development in the Verification Support Environment (VSE)

This page was built for publication: Using answer set programming in the development of verified software

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5398045)