scientific article; zbMATH DE number 7552282
DOI10.13137/2464-8728/33309zbMath1490.68079arXiv2104.08130MaRDI QIDQ5087785
Maximiliano Cristiá, Gianfranco Rossi
Publication date: 1 July 2022
Full work available at URL: https://arxiv.org/abs/2104.08130
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Theory of programming languages (68N15) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Applications of set theory (03E75) Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Other classical set theory (including functions, relations, and set algebra) (03E20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Uses Software
Cites Work
- A pearl on SAT and SMT solving in Prolog
- The calculus of constructions
- A set solver for finite set relation algebra
- Abstract state machines, Alloy, B, TLA, VDM, and Z. 6th international conference, ABZ 2018, Southampton, UK, June 5--8, 2018. Proceedings
- Cardinality constraints for arrays (decidability results and applications)
- Automated proof of Bell-LaPadula security properties
- An automatically verified prototype of the Tokeneer ID station specification
- Efficient automated reasoning about sets and multisets with cardinality constraints
- Solving quantifier-free first-order constraints over finite sets and binary relations
- A complete and terminating approach to linear integer solving
- A decision procedure for restricted intensional sets
- Automated reasoning with restricted intensional sets
- {log}: A language for programming in logic with finite sets
- Proofs as programs
- Set unification
- A Decision Procedure for Sets, Binary Relations and Partial Functions
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: