Encoding OCL Data Types for SAT-Based Verification of UML/OCL Models

DOI10.1007/978-3-642-21768-5_12zbMath1335.68070DBLPconf/tap/SoekenWD11OpenAlexW1494631286WikidataQ59242557 ScholiaQ59242557MaRDI QIDQ3012970

Mathias Soeken, Robert Wille, Rolf Drechsler

Publication date: 7 July 2011

Published in: Tests and Proofs (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-21768-5_12

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

A framework for model transformation verification ⋮ Encoding OCL Data Types for SAT-Based Verification of UML/OCL Models ⋮ Intra- and interdiagram consistency checking of behavioral multiview models

Uses Software

• Boolector
• MiniSat
• Chaff
• BerkMin
• UML2Alloy

Cites Work

• Real quantifier elimination is doubly exponential
• BerkMin: A fast and robust SAT-solver
• Encoding OCL Data Types for SAT-Based Verification of UML/OCL Models
• Computer Aided Verification
• Theory and Applications of Satisfiability Testing
• Mechanizing Mathematical Reasoning

This page was built for publication: Encoding OCL Data Types for SAT-Based Verification of UML/OCL Models