Towards Certified Model Checking for PLTL using One-pass Tableaux
- Submitting institution
-
The University of Westminster
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- qw728
- Type
- E - Conference contribution
- DOI
-
10.4230/LIPIcs.TIME.2019.12
- Title of conference / published proceedings
- Leibniz International Proceedings in Informatics
- First page
- 12:1
- Volume
- 147
- Issue
- -
- ISSN
- 1868-8969
- Open access status
- Compliant
- Month of publication
- October
- Year of publication
- 2019
- URL
-
https://drops.dagstuhl.de/opus/volltexte/2019/11370/
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
4
- Research group(s)
-
-
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Desired properties of complex software systems are verified in mathematical models required by software certification standards. Here counter-examples are useful in fixing errors. However, often explicit proofs certifying the satisfiability of properties are needed. This paper is significant because it defines one novel temporal reasoning mechanism for both counterexamples and certificates. With its rigour ensured by relevant mathematical proofs and potential optimisation by embedding SAT solvers, the approach has been investigated in industrial setting to meet European Standards for Safety Critical Systems. These statements can be evidenced by Jorge Parra, Head of Dependable Software team, Ikerlan Technology Research Centre: JParra@ikerlan.es.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
