3 papers · 1 filter
PolyQEnt: A Polynomial Quantified Entailment Solver
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady +4
Polynomial quantified entailments with existentially and universally quantified variables arise in many problems of verification and program analysis. We present PolyQEnt which is…
Fixed Point Certificates for Reachability and Expected Rewards in MDPs
Krishnendu Chatterjee, Tim Quatmann, Maximilian Schäffeler +3
The possibility of errors in human-engineered formal verification software, such as model checkers, poses a serious threat to the purpose of these tools. An established approach to…
Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization
Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Mehrdad Karrabi +3
The problem of checking satisfiability of linear real arithmetic (LRA) and non-linear real arithmetic (NRA) formulas has broad applications, in particular, they are at the heart of…