Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants (Q4913868): Difference between revisions

Latest revision as of 08:33, 6 July 2024

scientific article; zbMATH DE number 6154727

Language	Label	Description	Also known as
English	Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants	scientific article; zbMATH DE number 6154727

Statements

instance of

scholarly article

0 references

title

Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants (English)

0 references

0 references

0 references

0 references

0 references

0 references

0 references

Automated Reasoning and Mathematics

0 references

publication date

16 April 2013

0 references

describes a project that uses

ASTREE

0 references

MaRDI profile type

MaRDI publication profile

0 references

full work available at URL

https://doi.org/10.1007/978-3-642-36675-8_11

0 references

cites work

Inferring Min and Max Invariants Using Max-Plus Polyhedra

0 references

An Improved Tight Closure Algorithm for Integer Octagonal Constraints

0 references

Hard problems in max-algebra, control theory, hypergraphs and other areas

0 references

Q4414726

0 references

Max-linear Systems: Theory and Algorithms

0 references

Ranking Abstractions

0 references

Programming Languages and Systems

0 references

Abstract Interpretation Frameworks

0 references

Avoiding exponential explosion

0 references

Max-Plus Convex Geometry

0 references

Constraint-Based Approach for Analysis of Hybrid Systems

0 references

Abstractions from proofs

0 references

An axiomatic basis for computer programming

0 references

A quantifier-elimination based heuristic for automatically generating inductive assertions for programs

0 references

Applying Linear Quantifier Elimination

0 references

Non-linear loop invariant generation using Gröbner bases

0 references

Theory and Applications of Satisfiability Testing

0 references

From program verification to program synthesis

0 references

Verification and synthesis using real quantifier elimination

0 references

Synthesizing Switching Logic Using Constraint Solving

0 references

Termination of linear programs with nonlinear constraints

0 references

Recent advances in program verification through computer algebra

0 references

Q4140769

0 references

Identifiers

zbMATH Open document ID

1385.68013

0 references

DOI

10.1007/978-3-642-36675-8_11

0 references

Mathematics Subject Classification ID

0 references

0 references

0 references

0 references

0 references

Sitelinks

Mathematics(1 entry)

mardi Publication:4913868

@@ Property / author @@
-Heng-Jun Zhao
@@ Property / author: Heng-Jun Zhao / rank @@
-Normal rank
@@ Property / author @@
+Heng-Jun Zhao
@@ Property / author: Heng-Jun Zhao / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ASTREE
@@ Property / describes a project that uses: ASTREE / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-642-36675-8_11
+Normal rank
@@ Property / OpenAlex ID @@
+W39834257
@@ Property / OpenAlex ID: W39834257 / rank @@
+Normal rank
@@ Property / cites work @@
+Inferring Min and Max Invariants Using Max-Plus Polyhedra
+Normal rank
@@ Property / cites work @@
+An Improved Tight Closure Algorithm for Integer Octagonal Constraints
+Normal rank
@@ Property / cites work @@
+Hard problems in max-algebra, control theory, hypergraphs and other areas
+Normal rank
@@ Property / cites work @@
+Q4414726
@@ Property / cites work: Q4414726 / rank @@
+Normal rank
@@ Property / cites work @@
+Max-linear Systems: Theory and Algorithms
@@ Property / cites work: Max-linear Systems: Theory and Algorithms / rank @@
+Normal rank
@@ Property / cites work @@
+Ranking Abstractions
@@ Property / cites work: Ranking Abstractions / rank @@
+Normal rank
@@ Property / cites work @@
+Programming Languages and Systems
@@ Property / cites work: Programming Languages and Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Abstract Interpretation Frameworks
@@ Property / cites work: Abstract Interpretation Frameworks / rank @@
+Normal rank
@@ Property / cites work @@
+Avoiding exponential explosion
@@ Property / cites work: Avoiding exponential explosion / rank @@
+Normal rank
@@ Property / cites work @@
+Max-Plus Convex Geometry
@@ Property / cites work: Max-Plus Convex Geometry / rank @@
+Normal rank
@@ Property / cites work @@
+Constraint-Based Approach for Analysis of Hybrid Systems
+Normal rank
@@ Property / cites work @@
+Abstractions from proofs
@@ Property / cites work: Abstractions from proofs / rank @@
+Normal rank
@@ Property / cites work @@
+An axiomatic basis for computer programming
@@ Property / cites work: An axiomatic basis for computer programming / rank @@
+Normal rank
@@ Property / cites work @@
+A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
+Normal rank
@@ Property / cites work @@
+Applying Linear Quantifier Elimination
@@ Property / cites work: Applying Linear Quantifier Elimination / rank @@
+Normal rank
@@ Property / cites work @@
+Non-linear loop invariant generation using Gröbner bases
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+From program verification to program synthesis
@@ Property / cites work: From program verification to program synthesis / rank @@
+Normal rank
@@ Property / cites work @@
+Verification and synthesis using real quantifier elimination
+Normal rank
@@ Property / cites work @@
+Synthesizing Switching Logic Using Constraint Solving
+Normal rank
@@ Property / cites work @@
+Termination of linear programs with nonlinear constraints
+Normal rank
@@ Property / cites work @@
+Recent advances in program verification through computer algebra
+Normal rank
@@ Property / cites work @@
+Q4140769
@@ Property / cites work: Q4140769 / rank @@
+Normal rank