DOI10.1145/964001.964028zbMath1325.68071OpenAlexW2098045685MaRDI QIDQ3452270
Zohar Manna, Sriram Sankaranarayanan, Henny B. Sipma
Publication date: 11 November 2015
Published in: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.137.9536
Analysis of linear definite iterative loops,
Combining Model Checking and Data-Flow Analysis,
Computing polynomial program invariants,
Recent advances in program verification through computer algebra,
A deductive approach towards reasoning about algebraic transition systems,
Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems,
A quantifier-elimination based heuristic for automatically generating inductive assertions for programs,
Formal Modelling, Analysis and Verification of Hybrid Systems,
On invariant checking,
Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods,
The structure of polynomial invariants of linear loops,
Transformation-Enabled Precondition Inference,
Local Search For Satisfiability Modulo Integer Arithmetic Theories,
Resource-usage-aware configuration in software product lines,
Change-of-bases abstractions for non-linear hybrid systems,
A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis,
Generating invariants for non-linear loops by linear algebraic methods,
SAT modulo linear arithmetic for solving polynomial constraints,
Analysing All Polynomial Equations in ${\mathbb Z_{2^w}}$,
Formal verification and quantitative metrics of MPSoC data dynamics,
Algebra, Coalgebra, and Minimization in Polynomial Differential Equations,
Polynomial invariants for linear loops,
Generating all polynomial invariants in simple loops,
Toward automatic verification of quantum programs,
Counterexample- and simulation-guided floating-point loop invariant synthesis,
Algebra-based synthesis of loops and their invariants (invited paper),
An Iterative Method for Generating Loop Invariants,
Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants,
Constructing invariants for hybrid systems,
Elimination Techniques for Program Analysis,
Loop invariants,
Inferring Loop Invariants Using Postconditions,
A method of proving the invariance of linear inequalities for linear loops,
Generalized homogeneous polynomials for efficient template-based nonlinear invariant synthesis,
Invariant Synthesis for Combined Theories,
Reasoning Algebraically About P-Solvable Loops,
Automatic pre- and postconditions for partial differential equations,
On the Coalgebra of Partial Differential Equations,
Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants,
Mathematics for reasoning about loop functions,
O-Minimal Invariants for Discrete-Time Dynamical Systems,
Endomorphisms for Non-trivial Non-linear Loop Invariant Generation,
Discovering non-terminating inputs for multi-path polynomial programs
