Search results for "presburger arithmetic"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
3	Felix Klaedtke	Bounds on the automata size for Presburger arithmetic.	ACM Trans. Comput. Log.	2008	DBLP DOI BibTeX RDF	Automata-based decision procedures, complexity, quantifier elimination, Presburger arithmetic
3	Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard	Deciding Boolean Algebra with Presburger Arithmetic.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF	complexity, program verification, decision procedure, Boolean algebra, quantifier elimination, Presburger arithmetic
2	Aless Lasaruk, Thomas Sturm	Effective Quantifier Elimination for Presburger Arithmetic with Infinity.	CASC	2009	DBLP DOI BibTeX RDF
2	Mathias Barra	A Characterisation of the Relations Definable in Presburger Arithmetic.	TAMC	2008	DBLP DOI BibTeX RDF
2	Véronique Bruyère, Emmanuel Dall'Olio, Jean-François Raskin	Durations and parametric model-checking in timed automata.	ACM Trans. Comput. Log.	2008	DBLP DOI BibTeX RDF	model-checking, Timed automata, Presburger arithmetic
2	Alexander Rybalov	Generic Complexity of Presburger Arithmetic.	CSR	2007	DBLP DOI BibTeX RDF
2	Viktor Kuncak, Martin C. Rinard	Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic.	CADE	2007	DBLP DOI BibTeX RDF
2	K. Subramani	Tractable Fragments of Presburger Arithmetic.	Theory Comput. Syst.	2005	DBLP DOI BibTeX RDF
2	Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard	An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic.	CADE	2005	DBLP DOI BibTeX RDF
2	Amine Chaieb, Tobias Nipkow	Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic.	LPAR	2005	DBLP DOI BibTeX RDF
2	Nicole Schweikardt	Arithmetic, first-order logic, and counting quantifiers.	ACM Trans. Comput. Log.	2005	DBLP DOI BibTeX RDF	Counting quantifiers, first-order logic, quantifier elimination, Presburger arithmetic
2	Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman	Abstraction-Based Satisfiability Solving of Presburger Arithmetic.	CAV	2004	DBLP DOI BibTeX RDF
2	Felix Klaedtke	On the Automata Size for Presburger Arithmetic.	LICS	2004	DBLP DOI BibTeX RDF
2	Lavinia Egidi, Paolo Terenziani	A Mathematical Framework for the Semantics of Symbolic Languages Representing Periodic Time.	TIME	2004	DBLP DOI BibTeX RDF	user-defined periodicity, semantics, Presburger Arithmetic, symbolic languages
2	Hyun Suk Kim, Narayanan Vijaykrishnan, Mahmut T. Kandemir, Erik Brockmeyer, Francky Catthoor, Mary Jane Irwin	Estimating influence of data layout optimizations on SDRAM energy consumption.	ISLPED	2003	DBLP DOI BibTeX RDF	Ehrhart polynomial, Omega calculator, page break, energy, data locality, data layout, Presburger arithmetic, SDRAM
2	Vijay Ganesh, Sergey Berezin, David L. Dill	Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods.	FMCAD	2002	DBLP DOI BibTeX RDF
2	William Pugh, David Wonnacott	Constraint-Based Array Dependence Analysis.	ACM Trans. Program. Lang. Syst.	1998	DBLP DOI BibTeX RDF	array dataflow analysis, dependence abstraction, parallelization, static analysis, dependence analysis, Presburger Arithmetic
2	Laurent Fribourg, Hans Olsén	Proving Safety Properties of Infinite State Systems by Compilation into Presburger Arithmetic.	CONCUR	1997	DBLP DOI BibTeX RDF
2	Alexandre Boudet, Hubert Comon	Diophantine Equations, Presburger Arithmetic and Finite Automata.	CAAP	1996	DBLP DOI BibTeX RDF
2	Teruo Higashino, Gregor von Bochmann	Automatic Analysis and Test Case Derivation for a Restricted Class of LOTOS Expressions with Data Parameters.	IEEE Trans. Software Eng.	1994	DBLP DOI BibTeX RDF	test case derivation, LOTOS expressions, data parameters, automatic analysis method, P-LOTOS expressions, Boolean types, integer linear programming problems, deadlock detection problem, nonexecutable branch detection, nondeterministic behavior detection, simplified Session protocol, formal specification, linear programming, concurrency control, integer programming, specification languages, specification language, comparison, decision procedure, data types, addition, test selection, Presburger arithmetic, subtraction, integer, data values
1	Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl	An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.	J. Autom. Reasoning	2011	DBLP DOI BibTeX RDF
1	Michael R. Hansen, Aske Wiid Brekling	On Tool Support for Duration Calculus on the Basis of Presburger Arithmetic.	TIME	2011	DBLP DOI BibTeX RDF
1	Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl	Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic.	VMCAI	2011	DBLP DOI BibTeX RDF
1	Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl	Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Extended Technical Report)	CoRR	2010	DBLP BibTeX RDF
1	Alexander Rybalov	Generic Complexity of Presburger Arithmetic.	Theory Comput. Syst.	2010	DBLP DOI BibTeX RDF
1	Antoine Durand-Gasselin, Peter Habermehl	On the Use of Non-deterministic Automata for Presburger Arithmetic.	CONCUR	2010	DBLP DOI BibTeX RDF
1	Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl	An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.	IJCAR	2010	DBLP DOI BibTeX RDF
1	Daniel Kroening, Jérôme Leroux, Philipp Rümmer	Interpolating Quantifier-Free Presburger Arithmetic.	LPAR (Yogyakarta)	2010	DBLP DOI BibTeX RDF
1	Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter	Complete functional synthesis.	PLDI	2010	DBLP DOI BibTeX RDF	bapa, synthesis procedure, decision procedure, presburger arithmetic
1	Jérôme Leroux, Gérald Point	TaPAS: The Talence Presburger Arithmetic Suite.	TACAS	2009	DBLP DOI BibTeX RDF
1	Zijiang Yang, Chao Wang, Aarti Gupta, Franjo Ivancic	Model checking sequential software programs via mixed symbolic analysis.	ACM Trans. Design Autom. Electr. Syst.	2009	DBLP DOI BibTeX RDF	composite symbolic formula, Model checking, binary decision diagram, reachability analysis, presburger arithmetic, image computation
1	Stefan Göller, Richard Mayr, Anthony Widjaja To	On the Computational Complexity of Verifying One-Counter Processes.	LICS	2009	DBLP DOI BibTeX RDF
1	Jérôme Leroux	The General Vector Addition System Reachability Problem by Presburger Inductive Invariants.	LICS	2009	DBLP DOI BibTeX RDF
1	Guanhua He, Chenguang Luo	Heap Memory Requirements Analysis via Separation Logic.	TASE	2009	DBLP DOI BibTeX RDF
1	Stephan Falke, Deepak Kapur	A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs.	CADE	2009	DBLP DOI BibTeX RDF
1	Christoph Haase, Stephan Kreutzer, Joël Ouaknine, James Worrell	Reachability in Succinct and Parametric One-Counter Automata.	CONCUR	2009	DBLP DOI BibTeX RDF
1	Anthony Widjaja To	Model Checking FO(R) over One-Counter Processes and beyond.	CSL	2009	DBLP DOI BibTeX RDF
1	Thomas Wies, Ruzica Piskac, Viktor Kuncak	Combining Theories with Shared Set Operations.	FroCos	2009	DBLP DOI BibTeX RDF
1	Guillem Godoy, Ashish Tiwari	Invariant Checking for Programs with Procedure Calls.	SAS	2009	DBLP DOI BibTeX RDF
1	Marius Bozga, Codruta Gîrlea, Radu Iosif	Iterating Octagons.	TACAS	2009	DBLP DOI BibTeX RDF
1	Stefan Berghofer, Markus Reiter	Formalizing the Logic-Automaton Connection.	TPHOLs	2009	DBLP DOI BibTeX RDF
1	Angelo Brillout, Daniel Kroening, Thomas Wahl	Craig Interpolation for Quantifier-Free Presburger Arithmetic	CoRR	2008	DBLP BibTeX RDF
1	Chao Wang, Malay K. Ganai, Shuvendu K. Lahiri, Daniel Kroening	Embedded software verification: challenges and solutions.	ICCAD	2008	DBLP DOI BibTeX RDF
1	Axel Legay	T(O)RMC: A Tool for (omega)-Regular Model Checking.	CAV	2008	DBLP DOI BibTeX RDF
1	Mathias Barra	Pure Iteration and Periodicity.	CiE	2008	DBLP DOI BibTeX RDF
1	Mats Carlsson, Nicolas Beldiceanu, Julien Martin	A Geometric Constraint over k-Dimensional Objects and Shapes Subject to Business Rules.	CP	2008	DBLP DOI BibTeX RDF
1	Jochen Eisinger	Upper Bounds on the Automata Size for Integer and Mixed Real and Integer Linear Arithmetic (Extended Abstract).	CSL	2008	DBLP DOI BibTeX RDF
1	Philipp Rümmer	A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic.	LPAR	2008	DBLP DOI BibTeX RDF
1	Ruzica Piskac, Viktor Kuncak	Decision Procedures for Multisets with Cardinality Constraints.	VMCAI	2008	DBLP DOI BibTeX RDF
1	Tobias Schüle	Verification of infinite state systems using Presburger arithmetic.		2007	RDF
1	Shuvendu K. Lahiri, Krishna K. Mehra	Interpolant based Decision Procedure for Quantifier-Free Presburger Arithmetic.	JSAT	2007	DBLP BibTeX RDF
1	Tobias Nipkow	Reflecting Linear Arithmetic: From Dense Linear Orders to Presburger Arithmetic.	VERIFY	2007	DBLP BibTeX RDF
1	Christian Choffrut, Achille Frigeri	Definable sets in weak Presburger arithmetic.	ICTCS	2007	DBLP BibTeX RDF
1	Rathijit Sen, Y. N. Srikant	WCET estimation for executables in the presence of data caches.	EMSOFT	2007	DBLP DOI BibTeX RDF
1	Rona Machlin	Index-based multidimensional array queries: safety and equivalence.	PODS	2007	DBLP DOI BibTeX RDF	array query languages, integer linear constraints, aggregation, multidimensional data, scientific data, query equivalence
1	Stéphane Demri, Régis Gascon	The Effects of Bounding Syntactic Resources on Presburger LTL.	TIME	2007	DBLP DOI BibTeX RDF
1	Zohar Manna, Henny B. Sipma, Ting Zhang	Verifying Balanced Trees.	LFCS	2007	DBLP DOI BibTeX RDF
1	Aless Lasaruk, Thomas Sturm	Weak quantifier elimination for the full linear theory of the integers.	Appl. Algebra Eng. Commun. Comput.	2007	DBLP DOI BibTeX RDF	Integer constraint solving, Implementation, Quantifier elimination
1	Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli	Decision procedures for extensions of the theory of arrays.	Ann. Math. Artif. Intell.	2007	DBLP DOI BibTeX RDF	Mathematics Subject Classifications (2000) 68T27, 03B25, 03B70, 68T15
1	Stéphane Demri, Alain Finkel, Valentin Goranko, Govert van Drimmelen	Towards a Model-Checker for Counter Systems.	ATVA	2006	DBLP DOI BibTeX RDF
1	Bow-Yaw Wang	On the Satisfiability of Modular Arithmetic Formulae.	ATVA	2006	DBLP DOI BibTeX RDF
1	Tobias Schüle, Klaus Schneider	Verification of Data Paths Using Unbounded Integers: Automata Strike Back.	Haifa Verification Conference	2006	DBLP DOI BibTeX RDF
1	Marius Bozga, Radu Iosif, Yassine Lakhnech	Flat Parametric Counter Automata.	ICALP	2006	DBLP DOI BibTeX RDF
1	Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli	Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies.	JELIA	2006	DBLP DOI BibTeX RDF
1	Frédéric Blanqui, Colin Riba	Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems.	LPAR	2006	DBLP DOI BibTeX RDF
1	Aaron R. Bradley, Zohar Manna, Henny B. Sipma	What's Decidable About Arrays?	VMCAI	2006	DBLP DOI BibTeX RDF
1	Lavinia Egidi, Paolo Terenziani	A mathematical framework for the semantics of symbolic languages representing periodic time.	Ann. Math. Artif. Intell.	2006	DBLP DOI BibTeX RDF	AMS subject classification 68T30 Knowledge representation
1	Dana Angluin, James Aspnes, Zoë Diamadi, Michael J. Fischer, René Peralta	Computation in networks of passively mobile finite-state sensors.	Distributed Computing	2006	DBLP DOI BibTeX RDF	Finite-state agent, Intermittent communication, Stable computation, Mobile agent, Diffuse computation, Sensor net
1	Felix Klaedtke	Bounds on the Automata Size for Presburger Arithmetic	CoRR	2005	DBLP BibTeX RDF
1	Stefan S. Dantchev, Frank D. Valencia	On the computational limits of infinite satisfaction.	SAC	2005	DBLP DOI BibTeX RDF	infinite CSP, open CSP, decidability, constraint satisfaction problems
1	Thomas Sturm	Quantifier Elimination for Constraint Logic Programming.	CASC	2005	DBLP DOI BibTeX RDF
1	Gerd Behrmann, Kim Guldstrand Larsen, Jacob Illum Rasmussen	Beyond Liveness: Efficient Parameter Synthesis for Time Bounded Liveness.	FORMATS	2005	DBLP DOI BibTeX RDF
1	Marius Bozga, Radu Iosif	On Decidability Within the Arithmetic of Addition and Divisibility.	FoSSaCS	2005	DBLP DOI BibTeX RDF
1	Ting Zhang, Henny B. Sipma, Zohar Manna	Decision Procedures for Queues with Integer Constraints.	FSTTCS	2005	DBLP DOI BibTeX RDF
1	Wei-Ngan Chin, Huu Hai Nguyen, Shengchao Qin, Martin C. Rinard	Memory Usage Verification for OO Programs.	SAS	2005	DBLP DOI BibTeX RDF
1	Louis Latour	Computing Affine Hulls over Q and Z from Sets Represented by Number Decision Diagrams.	CIAA	2005	DBLP DOI BibTeX RDF
1	Silvano Dal-Zilio, Denis Lugiez, Charles Meyssonnier	A logic you can count on.	POPL	2004	DBLP DOI BibTeX RDF	semi-structured data, tree automata, substructural logic, Presburger arithmetic, ambient
1	Sanjit A. Seshia, Randal E. Bryant	Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds.	LICS	2004	DBLP DOI BibTeX RDF
1	Tobias Schüle, Klaus Schneider	Bounded model checking of infinite state systems: exploiting the automata hierarchy.	MEMOCODE	2004	DBLP DOI BibTeX RDF
1	David Déharbe, Abdessamad Imine, Silvio Ranise	Abstraction-Driven Verification of Array Programs.	AISC	2004	DBLP DOI BibTeX RDF
1	Xingyan Tian, Kejia Zhao, Huowang Chen, Hongyan Du	Cache Behavior Analysis of a Compiler-Assisted Cache Replacement Policy.	Asia-Pacific Computer Systems Architecture Conference	2004	DBLP DOI BibTeX RDF
1	Ting Zhang, Henny B. Sipma, Zohar Manna	Decision Procedures for Recursive Data Structures with Integer Constraints.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Stéphane Demri	LTL over Integer Periodicity Constraints: (Extended Abstract).	FoSSaCS	2004	DBLP DOI BibTeX RDF
1	Jörg H. Siekmann, Christoph Benzmüller	Omega: Computer Supported Mathematics.	KI	2004	DBLP DOI BibTeX RDF
1	Achim Blumensath, Erich Grädel	Finite Presentations of Infinite Structures: Automata and Interpretations.	Theory Comput. Syst.	2004	DBLP DOI BibTeX RDF
1	Andrei A. Muchnik	The definable criterion for definability in Presburger arithmetic and its applications.	Theor. Comput. Sci.	2003	DBLP DOI BibTeX RDF
1	Véronique Bruyère, Emmanuel Dall'Olio, Jean-François Raskin	Durations, Parametric Model-Checking in Timed Automata with Presburger Arithmetic.	STACS	2003	DBLP DOI BibTeX RDF
1	Helmut Seidl, Thomas Schwentick, Anca Muscholl	Numerical document queries.	PODS	2003	DBLP DOI BibTeX RDF	querying XML documents, XML, automata, monadic second order logic, Presburger arithmetic
1	Tuba Yavuz-Kahveci, Tevfik Bultan	A symbolic manipulator for automated verification of reactive systems with heterogeneous data types.	STTT	2003	DBLP DOI BibTeX RDF	Composite representation, BDD, Symbolic model checking, Presburger arithmetic
1	Tobias Schüle, Klaus Schneider	Exact Runtime Analysis Using Automata-Based Symbolic Simulation.	MEMOCODE	2003	DBLP DOI BibTeX RDF
1	Till Tantau	Weak Cardinality Theorems for First-Order Logic.	FCT	2003	DBLP DOI BibTeX RDF
1	Michael Norrish	Complete Integer Decision Procedures as Derived Rules in HOL.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Karl Lermer, Colin J. Fidge, Ian J. Hayes	Linear Approximation of Execution-Time Constraints.	Formal Asp. Comput.	2003	DBLP DOI BibTeX RDF	Automatic constraint determination, Real-time program analysis, Worst-case and best-case execution times, Control-flow analysis, Timing prediction
1	Yunjian Jiang, Robert K. Brayton	Don't Care Computation in Minimizing Extended Finite State Machines with Presburger Arithmetic.	IWLS	2002	DBLP BibTeX RDF
1	Slawomir Lasota	Decidability of Strong Bisimilarity for Timed BPP.	CONCUR	2002	DBLP DOI BibTeX RDF
1	Ofer Strichman	On Solving Presburger and Linear Arithmetic with SAT.	FMCAD	2002	DBLP DOI BibTeX RDF
1	Petr Jancar, Antonín Kucera, Faron Moller, Zdenek Sawa	Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds.	FoSSaCS	2002	DBLP DOI BibTeX RDF
1	Alessandro Armando, Silvio Ranise	A Practical Extension Mechanism for Decision Procedures: the Case Study of Universal Presburger Arithmetic.	J. UCS	2001	DBLP BibTeX RDF
1	Vlad Rusu, Elena Zinovieva	Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols.	Electr. Notes Theor. Comput. Sci.	2001	DBLP DOI BibTeX RDF
1	Mauricio Ayala-Rincón, Ivan E. Tavares de Araújo	Unification Modulo Presburger Arithmetic and Other Decidable Theories.	Revista Colombiana de Computación	2001	DBLP BibTeX RDF