Logic for Programming, Artificial Intelligence, and Reasoning

DOI10.1007/b106931zbMath1108.68410OpenAlexW4206255911MaRDI QIDQ5705937

Publication date: 10 November 2005

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/b106931

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Proving fairness and implementation correctness of a microkernel scheduler, Formal verification of C systems code. Structured types, separation logic and theorem proving, Formal memory models for the verification of low-level operating-system code, Balancing the load. Leveraging a semantics stack for systems verification, Types, Maps and Separation Logic, Mechanized semantics for the clight subset of the C language, HOL-Boogie -- an interactive prover-backend for the verifying C compiler, Introduction to ``Milestones in interactive theorem proving, Mechanising a type-safe model of multithreaded Java with a verified compiler, WhyMP, a formally verified arbitrary-precision integer library, Reasoning about memory layouts, Verified Characteristic Formulae for CakeML, A mechanical analysis of program verification strategies, Imperative Functional Programming with Isabelle/HOL, HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier, Verified Software Toolchain, CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs, Concerned with the unprivileged: user programs in kernel refinement, On the correctness of upper layers of automotive systems, Trustworthy Graph Algorithms (Invited Talk), Unnamed Item, Pervasive Theory of Memory, A Framework for the Automatic Formal Verification of Refinement from Cogent to C, Operating system verification---an overview, Proving the correctness of client/server software, Cogent: uniqueness types and certifying compilation, Modeling and Verifying Graph Transformations in Proof Assistants, A framework for the verification of certifying computations

Uses Software