Early verification of legal compliance via bounded satisfiability checking

DOI10.1007/978-3-031-37709-9_18MaRDI QIDQ6535696zbMATH OpenFDO

Authors Nick Feng, Lina Marsso, Mehrdad Sabetzadeh, Marsha Chechik

Publication date 1 February 2024

Copyright license Creative Commons Attribution 4.0 International

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• Time and compensation mechanisms in checking legal compliance
• Satisfiability checking for mission-time \textsf{LTL} (MLTL)
• Monitoring metric first-order temporal properties
• Real-time policy enforcement with metric first-order temporal logic
• Satisfiability checking for mission-time LTL

Cites work

• Accelerating LTL satisfiability checking by SAT solvers
• Benchmarking Model- and Satisfiability-Checking on Bi-infinite Time
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Constraint LTL satisfiability checking without automata
• Efficient E-Matching for SMT Solvers
• Model Checking Software
• Monitoring metric first-order temporal properties
• On the complexity of integer programming
• Quantifier instantiation techniques for finite model finding in SMT
• Real-time policy enforcement with metric first-order temporal logic
• Recursive unsolvability of a problem of Thue
• SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
• Satisfiability checking for mission-time LTL
• Simplify: a theorem prover for program checking
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• The Imandra Automated Reasoning System (System Description)

This page was built for publication: Early verification of legal compliance via bounded satisfiability checking

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