Search results for "existential quantification"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
2	Nicholas R. Cameron, Sophia Drossopoulou	Existential Quantification for Variant Ownership.	ESOP	2009	DBLP DOI BibTeX RDF
2	Makoto Tatsuta	Simple Saturated Sets for Disjunction and Second-Order Existential Quantification.	TLCA	2007	DBLP DOI BibTeX RDF
2	Carlos Grandón, Alexandre Goldsztejn	Inner approximation of distance constraints with existential quantification of parameters.	SAC	2006	DBLP DOI BibTeX RDF	AE-solution set, distance constraint, inner approximation, quantifier elimination, generalized intervals
2	Matthias Brantner, Sven Helmer, Carl-Christian Kanne, Guido Moerkotte	Kappa-Join: Efficient Execution of Existential Quantification in XML Query Languages.	XSym	2006	DBLP DOI BibTeX RDF
2	Orna Kupferman	Augmenting Branching Temporal Logics with Existential Quantification over Atomic Propositions.	CAV	1995	DBLP DOI BibTeX RDF
2	Kyu-Young Whang, Ashok Malhotra, Gary H. Sockut, Luanne M. Burns, Key-Sun Choi	Two-Dimensional Specification of Universal Quantification in a Graphical Database Query Language.	IEEE Trans. Software Eng.	1992	DBLP DOI BibTeX RDF	graphical database query language, universal quantification, existential quantification, direct representation, two-dimensional translation, existentially quantified two-dimensional queries, formal specification, relational databases, computer graphics, query languages, database theory, relational queries
1	Jörg Brauer, Andy King, Jael Kriener	Existential Quantification as Incremental SAT.	CAV	2011	DBLP DOI BibTeX RDF
1	Ross Tate, Juan Chen, Chris Hawblitzel	Inferable object-oriented typed assembly language.	PLDI	2010	DBLP DOI BibTeX RDF	existential quantification, object-oriented compiler, typed assembly language (tal), type inference, certifying compiler
1	Gerhard Jäger	Full operational set theory with unbounded existential quantification and power set.	Ann. Pure Appl. Logic	2009	DBLP DOI BibTeX RDF
1	Sagar Chaki, Arie Gurfinkel, Ofer Strichman	Decision diagrams for linear arithmetic.	FMCAD	2009	DBLP DOI BibTeX RDF
1	Matthew R. Lakin, Andrew M. Pitts	Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming.	ESOP	2009	DBLP DOI BibTeX RDF
1	Andreas Bauer 0002, Rajeev Goré, Alwen Tiu	A First-Order Policy Language for History-Based Transaction Monitoring.	ICTAC	2009	DBLP DOI BibTeX RDF
1	Colin Riba	On the Values of Reducibility Candidates.	TLCA	2009	DBLP DOI BibTeX RDF
1	Patricia Johann, Neil Ghani	Foundations for structured programming with GADTs.	POPL	2008	DBLP DOI BibTeX RDF	program fusion, GADTs, initial algebra semantics
1	Gilles Barthe, Benjamin Grégoire, Colin Riba	Type-Based Termination with Sized Products.	CSL	2008	DBLP DOI BibTeX RDF
1	Huu Hai Nguyen, Viktor Kuncak, Wei-Ngan Chin	Runtime Checking for Separation Logic.	VMCAI	2008	DBLP DOI BibTeX RDF
1	Marc Bezem, Dimitri Hendriks	On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Coherent logic, Proof objects, Hessenberg’s theorem, Automated theorem proving
1	Sumit Gulwani, Ashish Tiwari	An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software.	CAV	2007	DBLP DOI BibTeX RDF
1	Stefan Wehr, Ralf Lämmel, Peter Thiemann	JavaGI : Generalized Interfaces for Java.	ECOOP	2007	DBLP DOI BibTeX RDF
1	Maria Grazia Buscemi, Ugo Montanari	CC-Pi: A Constraint-Based Language for Specifying Service Level Agreements.	ESOP	2007	DBLP DOI BibTeX RDF
1	Carlos Olarte, Catuscia Palamidessi, Frank Valencia	Universal Timed Concurrent Constraint Programming.	ICLP	2007	DBLP DOI BibTeX RDF
1	Sean Weaver, John V. Franco, John S. Schlipf	Extending Existential Quantification in Conjunctions of BDDs.	JSAT	2006	DBLP BibTeX RDF
1	Sumit Gulwani, Ashish Tiwari	Combining abstract interpreters.	PLDI	2006	DBLP DOI BibTeX RDF	Nelson-Oppen combination, logical product, reduced product, abstract interpreter
1	Polyvios Pratikakis, Jeffrey S. Foster, Michael W. Hicks	LOCKSMITH: context-sensitive correlation analysis for race detection.	PLDI	2006	DBLP DOI BibTeX RDF	locksmith, correlation, type inference, context-sensitivity, race detection, multi-threaded programming
1	Zoltan Somogyi, Konstantinos F. Sagonas	Tabling in Mercury: Design and Implementation.	PADL	2006	DBLP DOI BibTeX RDF
1	Polyvios Pratikakis, Jeffrey S. Foster, Michael Hicks	Existential Label Flow Inference Via CFL Reachability.	SAS	2006	DBLP DOI BibTeX RDF
1	Yuliya Zabiyaka, Adnan Darwiche	Functional Treewidth: Bounding Complexity in the Presence of Functional Dependencies.	SAT	2006	DBLP DOI BibTeX RDF
1	Gianpiero Cabodi, Marco Crivellari, Sergio Nocco, Stefano Quer	Circuit Based Quantification: Back to State Set Manipulation within Unbounded Model Checking.	DATE	2005	DBLP DOI BibTeX RDF
1	Martin Hofmann	Proof-Theoretic Approach to Description-Logic.	LICS	2005	DBLP DOI BibTeX RDF
1	Hyeong-Ju Kang, In-Cheol Park	SAT-based unbounded symbolic model checking.	IEEE Trans. on CAD of Integrated Circuits and Systems	2005	DBLP DOI BibTeX RDF
1	Stéphane Demri, Régis Gascon	Verification of Qualitative Constraints.	CONCUR	2005	DBLP DOI BibTeX RDF
1	Andrea Ferrara, Guoqiang Pan, Moshe Y. Vardi	Treewidth in Verification: Local vs. Global.	LPAR	2005	DBLP DOI BibTeX RDF
1	Guoqiang Pan, Moshe Y. Vardi	Symbolic Techniques in Satisfiability Solving.	J. Autom. Reasoning	2005	DBLP DOI BibTeX RDF	symbolic decision procedure, satisfiability, binary decision diagram
1	Malay K. Ganai, Aarti Gupta, Pranav Ashar	Efficient SAT-based unbounded symbolic model checking using circuit cofactoring.	ICCAD	2004	DBLP DOI BibTeX RDF
1	Joshua Dunfield, Frank Pfenning	Tridirectional typechecking.	POPL	2004	DBLP DOI BibTeX RDF	type refinements, dependent types, intersection types, union types
1	Dominik Stoffel, Markus Wedler, Peter Warkentin, Wolfgang Kunz	Structural FSM traversal.	IEEE Trans. on CAD of Integrated Circuits and Systems	2004	DBLP DOI BibTeX RDF
1	Hubie Chen	Quantified Constraint Satisfaction and 2-Semilattice Polymorphisms.	CP	2004	DBLP DOI BibTeX RDF
1	Guoqiang Pan, Moshe Y. Vardi	Search vs. Symbolic Techniques in Satisfiability Solving.	SAT (Selected Papers	2004	DBLP DOI BibTeX RDF
1	Hyeong-Ju Kang, In-Cheol Park	SAT-based unbounded symbolic model checking.	DAC	2003	DBLP DOI BibTeX RDF	boolean satisfiability checking, unbounded symbolic model checking, formal verification, symbolic model checking
1	Andreas Rossberg	Generativity and dynamic opacity for abstract types.	PPDP	2003	DBLP DOI BibTeX RDF	generativity, encapsulation, opacity, dynamic typing, abstract types, existential types
1	Viktor Kuncak, Martin C. Rinard	Existential Heap Abstraction Entailment Is Undecidable.	SAS	2003	DBLP DOI BibTeX RDF	Program Verification, Shape Analysis, Type Checking, Monadic Second-Order Logic, Typestate, Graph Homomorphism, Post Correspondence Problem
1	Jirí Srba	Undecidability of Weak Bisimilarity for PA-Processes.	Developments in Language Theory	2002	DBLP DOI BibTeX RDF
1	Julia Klinger	Semiconcept Graphs with Variables.	ICCS	2002	DBLP DOI BibTeX RDF
1	Iliano Cervesato, Nancy A. Durgin, Patrick Lincoln, John C. Mitchell, Andre Scedrov	A Comparison between Strand Spaces and Multiset Rewriting for Security Protocol Analysis.	ISSS	2002	DBLP DOI BibTeX RDF
1	John C. Mitchell	Multiset Rewriting and Security Protocol Analysis.	RTA	2002	DBLP DOI BibTeX RDF
1	Alfonso San Miguel Aguirre, Moshe Y. Vardi	Random 3-SAT and BDDs: The Plot Thickens Further.	CP	2001	DBLP DOI BibTeX RDF
1	Iliano Cervesato, Nancy A. Durgin, John C. Mitchell, Patrick Lincoln, Andre Scedrov	Relating Strands and Multiset Rewriting for Security Protocol Analysis. (PDF / PS)	CSFW	2000	DBLP DOI BibTeX RDF
1	Krzysztof R. Apt	A Denotational Semantics for First-Order Logic.	Computational Logic	2000	DBLP DOI BibTeX RDF
1	Deepak D'Souza	A Logical Characterisation of Event Recording Automata.	FTRTFT	2000	DBLP DOI BibTeX RDF
1	Orna Kupferman	Augmenting Branching Temporal Logics with Existential Quantification over Atomic Propositions.	J. Log. Comput.	1999	DBLP DOI BibTeX RDF
1	Sela Mador-Haim, Limor Fix	Input Elimination and Abstraction in Model Checking.	FMCAD	1998	DBLP DOI BibTeX RDF
1	Martin Müller, Joachim Niehren	Ordering Constraints over Feature Trees Expressed in Second-Order Monadic Logic.	RTA	1998	DBLP DOI BibTeX RDF
1	Pavel Materna	Rules of Existential Quantification into "Intensional Contexts".	Studia Logica	1997	DBLP DOI BibTeX RDF
1	Gianpiero Cabodi, Paolo Camurati	Symbolic FSM traversals based on the transition relation.	IEEE Trans. on CAD of Integrated Circuits and Systems	1997	DBLP DOI BibTeX RDF
1	Gwen Kerdiles, Eric Salvat	A Sound and Complete CG Proof Procedure Combining Projections with Analytic Tableaux.	ICCS	1997	DBLP DOI BibTeX RDF
1	Michael R. Donat	Automating Formal Specification-Based Testing.	TAPSOFT	1997	DBLP DOI BibTeX RDF
1	Sang-goo Lee, Dong-Hoon Choi, Sang-Ho Lee	A Logic Database System with Extended Functionality. (PDF / PS)	COMPSAC	1996	DBLP DOI BibTeX RDF
1	Amy P. Felty	Proof Search with Set Variable Instantiation in the Calculus of Constructions.	CADE	1996	DBLP DOI BibTeX RDF
1	Goetz Graefe, Richard L. Cole	Fast Algorithms for Universal Quantification in Large Databases.	ACM Trans. Database Syst.	1995	DBLP DOI BibTeX RDF
1	Andrea Schaerf	On the Complexity of the Instance Checking Problem in Concept Languages with Existential Quantification.	J. Intell. Inf. Syst.	1993	DBLP DOI BibTeX RDF
1	Andrea Schaerf	On the Complexity of the Instance Checking Problem in Concept Languages with Existential Quantification.	ISMIS	1993	DBLP DOI BibTeX RDF
1	Francesco M. Donini, Maurizio Lenzerini, Daniele Nardi, Bernhard Hollunder, Werner Nutt, Alberto Marchetti-Spaccamela	The Complexity of Existential Quantification in Concept Languages.	Artif. Intell.	1992	DBLP DOI BibTeX RDF
1	Karen L. Kwast, Sieger van Denneheuvel	Weak Implication: Theory and Applications.	JELIA	1992	DBLP DOI BibTeX RDF
1	Prakash Panangaden, Vijay A. Saraswat, Philip J. Scott, R. A. G. Seely	A Hyperdoctrinal View of Concurrent Constraint Programming.	REX Workshop	1992	DBLP DOI BibTeX RDF	hyperdoctrines, constraint programs, asynchronous systems, closure operators, fibrations
1	Claudio Fratarcangeli	Technique for Universal Quantification in SQL.	SIGMOD Record	1991	DBLP DOI BibTeX RDF	SQL
1	Martín Abadi	An Axiomatization of Lamport's Temporal Logic of Actions.	CONCUR	1990	DBLP DOI BibTeX RDF