This paper introduces a uniform substitution calculus for
dℒ_CHP, the dy...
This paper presents a dynamic logic dℒ_CHP for
compositional deductive v...
Invariant sets are a key ingredient for verifying safety and other prope...
We formalize a multivariate quantifier elimination (QE) algorithm in the...
We propose a new approach to automated theorem proving and deductive pro...
Definition packages in theorem provers provide users with means of defin...
This paper investigates first-order game logic and first-order modal
mu-...
Switched systems are known to exhibit subtle (in)stability behaviors
req...
Many cyber-physical systems (CPS) are safety-critical, so it is importan...
The design of aircraft collision avoidance algorithms is a subtle but
im...
This paper presents a formally verified quantifier elimination (QE) algo...
We formalize the univariate fragment of Ben-Or, Kozen, and Reif's (BKR)
...
Real world systems of interest often feature interactions between discre...
Stability is required for real world controlled systems as it ensures th...
Continuous invariants are an important component in deductive verificati...
This article presents an axiomatic approach for deductive verification o...
Game Logic is an excellent setting to study proofs-about-programs via th...
We extend the constructive differential game logic (CdGL) of hybrid game...
Hybrid games are models which combine discrete, continuous, and adversar...
Cyber-physical systems (CPSs) are important whenever computer technology...
We present Kaisar, a structured interactive proof language for different...
This article proves the completeness of an axiomatization for differenti...
Some hybrid systems models are unsafe for mathematically correct but
phy...
This paper presents an approach for deductive liveness verification for
...
We formally prove end-to-end correctness of a ground robot implemented i...
Uniform substitution of function, predicate, program or game symbols is ...
Uniform substitution of function, predicate, program or game symbols is ...
The desire to use reinforcement learning in safety-critical settings has...
Programmable Logic Controllers (PLCs) provide a prominent choice of
impl...
Formal verification provides strong safety guarantees about models of
cy...
This paper presents a uniform substitution calculus for differential gam...
We prove the completeness of an axiomatization for differential equation...