A formalization of programs in first-order logic with a discrete linear order

DOI10.1016/j.artint.2016.01.014zbMath1352.68065OpenAlexW2264437737MaRDI QIDQ274400

Fangzhen Lin

Publication date: 22 April 2016

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.artint.2016.01.014

zbMATH Keywords

first-order logicprogram semanticsreasoning about programs

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

\textsc{Diffy}: inductive reasoning of array programs using difference invariants

Uses Software

• GOLOG
• Daikon

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Elements of finite model theory.
• The temporal semantics of concurrent programs
• First-order dynamic logic
• Automatic generation of invariants and intermediate assertions
• The Daikon system for dynamic detection of likely invariants
• Tight, consistent, and computable completions for unrestricted logic programs
• GOLOG: A logic programming language for dynamic domains
• Program verification through characteristic formulae
• Characteristic formulae for the verification of imperative programs
• The synthesis of loop predicates
• An axiomatic basis for computer programming

This page was built for publication: A formalization of programs in first-order logic with a discrete linear order