From model completeness to verification of data aware processes

DOI10.1007/978-3-030-22102-7_10zbMath1443.68103OpenAlexW2955627368MaRDI QIDQ2185467

Diego Calvanese, Marco Montali, Alessandro Gianola, Silvio Ghilardi, Andrey Rivkin

Publication date: 4 June 2020

Full work available at URL: https://doi.org/10.1007/978-3-030-22102-7_10

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (6)

SMT-based verification of data-aware processes: a model-theoretic approach ⋮ Interpolation and amalgamation for arrays with MaxDiff ⋮ Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) ⋮ Model completeness, covers and superposition ⋮ Combination of uniform interpolants via Beth definability ⋮ Combined covers and Beth definability

Uses Software

• Yices
• ASASP
• Mcmt
• Cubicle
• SAFARI
• Booster
• VERIFAS

This page was built for publication: From model completeness to verification of data aware processes