Computing Program Reliability Using Forward-Backward Precondition Analysis and Model Counting

DOI10.1007/978-3-030-45234-6_9MaRDI QIDQ5039530zbMATH OpenOpenAlexFDO

Authors Aleksandar Dimovski, Axel Legay

Publication date 13 October 2022

Published in Fundamental Approaches to Software Engineering (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-45234-6_9

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Quantifying software reliability via model-counting
• Computing software reliability based on program invariants
• A general theory of software-reliability modeling
• scientific article; zbMATH DE number 4018190
• Formal dependability modeling and analysis: a survey
• Dependability modeling and analysis of distributed programs

Cites work

• Abstract interpretation and application to logic programs
• Abstraction, Refinement and Proof for Probabilistic Systems
• Algorithm for finding a general formula for the non-negative solutions of a system of linear inequalities
• An abstract domain to infer ordinal-valued ranking functions
• An abstract Monte-Carlo method for the analysis of probabilistic programs
• Constructive versions of Tarski's fixed point theorems
• Dynamic partitioning in linear relation analysis: application to the verification of reactive systems
• Finding suitable variability abstractions for family-based analysis
• Finding suitable variability abstractions for lifted analysis
• Grammar Analysis and Parsing by Abstract Interpretation
• scientific article; zbMATH DE number 7445154 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Linear-invariant generation for probabilistic programs: automated support for proof-based methods
• Precondition inference from intermittent assertions and application to contracts on collections
• Probabilistic abstract interpretation
• Program verification using symbolic game semantics
• Static Analysis
• The octagon abstract domain

Cited in

(3)

• A decision tree lifted domain for analyzing program families with numerical features
• On calculating assertion probabilities for program families
• Quantifying software reliability via model-counting

Describes a project that uses

Uses Software

• Apron

This page was built for publication: Computing Program Reliability Using Forward-Backward Precondition Analysis and Model Counting

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