14 citations · 37 across the 7 of their papers we have counts for
8 papers
Verified Quadratic Virtual Substitution for Real Arithmetic
Matias Scharager, Katherine Cordwell, Stefan Mitsch +1
This paper presents a formally verified quantifier elimination (QE) algorithm for first-order real arithmetic by linear and quadratic virtual substitution (VS) in Isabelle/HOL. The…
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm
Katherine Cordwell, Yong Kiam Tan, André Platzer
We formalize the univariate fragment of Ben-Or, Kozen, and Reif's (BKR) decision procedure for first-order real arithmetic in Isabelle/HOL. BKR's algorithm has good potential for p…
Pegasus: Sound Continuous Invariant Generation
Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan +2
Continuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in d…
Towards Physical Hybrid Systems
Katherine Cordwell, André Platzer
Some hybrid systems models are unsafe for mathematically correct but physically unrealistic reasons. For example, mathematical models can classify a system as being unsafe on a set…
On algorithms to calculate integer complexity
Katherine Cordwell, Alyssa Epstein, Anand Hemmady +5
We consider a problem first proposed by Mahler and Popken in 1953 and later developed by Coppersmith, Erdős, Guy, Isbell, Selfridge, and others. Let be the complexity of $n…
On Near Perfect Numbers
Peter Cohen, Katherine Cordwell, Alyssa Epstein +3
The study of perfect numbers (numbers which equal the sum of their proper divisors) goes back to antiquity, and is responsible for some of the oldest and most popular conjectures i…
Summand minimality and asymptotic convergence of generalized Zeckendorf decompositions
Katherine Cordwell, Max Hlavacek, Chi Huynh +3
Given a recurrence sequence , with where for all and , the generalized Zeckendorf decomposi…
On Lower Central Series Quotients of Finitely Generated Algebras over
Katherine Cordwell, Teng Fei, Kathleen Zhou
Let be an associative unital algebra, its successive quotients of lower central series and the successive quotients of ideals generated by lower central series. The…