Integrating formal specifications into applications: the ProB Java API

DOI10.1007/s10703-020-00351-3zbMath1505.68024OpenAlexW3094156705MaRDI QIDQ2147695

Philipp Körner, Sebastian Krings, Jens Bendisposto, Michael Leuschel, Jannik Dunkelau

Publication date: 20 June 2022

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-020-00351-3

zbMATH Keywords

embeddingformal methodsJava APIProBrun-time execution

Mathematics Subject Classification ID

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

Uses Software

• CoreASM
• Modelica
• z3
• Rodin
• ProB
• Atelier B
• SICStus
• Overture Tool
• GitHub
• BTestBox
• EventB2Java
• JeB
• BMotionWeb
• VisB
• WebASM

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On correct refinement of programs
• An analysis of alpha-beta pruning
• Executing formal specifications with concurrent constraint programming
• Foundations of set theory. With the collaboration of Dirk van Dalen. 2nd revised ed
• Directed Model Checking for B: An Evaluation and New Techniques
• The B-Book
• Refinement Calculus
• FM 2005: Formal Methods
• Model Checking Software