scientific article; zbMATH DE number 6820296

DOI10.4230/LIPICS.ICALP.2016.107MaRDI QIDQ4598248zbMATH OpenFDO

Authors Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub

Publication date 19 December 2017

Full work available at URL https://arxiv.org/abs/1602.05681

zbMATH Keywords

accuracyformal verificationHoare logicprobabilistic algorithmsunion bound

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Recommendations

• Towards a logic for union types
• scientific article; zbMATH DE number 1332644
• scientific article; zbMATH DE number 4123706
• Synthesis of a unification algorithm in a logic programming calculus
• A decidable subtyping logic for intersection and union types
• Unification as a complexity measure for logic programming
• Bounded quantifications for iteration and concurrency in logic programming
• Bounds in the propagation of selection into logic programs
• scientific article; zbMATH DE number 219219
• Bounded nondeterminism of logic programs

Cited in

(5)

• Approximate relational Hoare logic for continuous random samplings
• Graded Hoare logic and its categorical semantics
• Unifying graded and parameterised monads
• BiGKAT: an algebraic framework for relational verification of probabilistic programs
• A Kleene algebra with tests for union bound reasoning about probabilistic programs

This page was built for publication:

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