Search results for "Edmund M. Clarke"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
1	Sicun Gao, Jeremy Avigad, Edmund M. Clarke	Delta-Decidability over the Reals	CoRR	2012	DBLP BibTeX RDF
1	Sicun Gao, Jeremy Avigad, Edmund M. Clarke	Delta-Complete Decision Procedures for Satisfiability over the Reals	CoRR	2012	DBLP BibTeX RDF
1	Edmund M. Clarke, Irina Virbitskaite, Andrei Voronkov (eds.)	Perspectives of Systems Informatics - 8th International Andrei Ershov Memorial Conference, PSI 2011, Novosibirsk, Russia, June 27-July 1, 2011, Revised Selected Papers	Ershov Memorial Conference	2012	DBLP DOI BibTeX RDF
1	Paolo Zuliani, Christel Baier, Edmund M. Clarke	Rare-event verification for stochastic hybrid systems.	HSCC	2012	DBLP DOI BibTeX RDF
1	Sicun Gao, André Platzer, Edmund M. Clarke	Quantifier Elimination over Finite Fields Using Gröbner Bases	CoRR	2011	DBLP BibTeX RDF
1	Sicun Gao, André Platzer, Edmund M. Clarke	Quantifier Elimination over Finite Fields Using Gröbner Bases.	CAI	2011	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Paolo Zuliani	Statistical Model Checking for Cyber-Physical Systems.	ATVA	2011	DBLP DOI BibTeX RDF
1	Haijun Gong, Paolo Zuliani, Qinsi Wang, Edmund M. Clarke	Formal analysis for logical models of pancreatic cancer.	CDC-ECE	2011	DBLP DOI BibTeX RDF
1	Ying-Chih Wang, Anvesh Komuravelli, Paolo Zuliani, Edmund M. Clarke	Analog circuit verification by statistical model checking.	ASP-DAC	2011	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Alexandre Donzé, Axel Legay	On simulation-based probabilistic model checking of mixed-analog circuits.	Formal Methods in System Design	2010	DBLP DOI BibTeX RDF
1	Sicun Gao, Malay K. Ganai, Franjo Ivancic, Aarti Gupta, Sriram Sankaranarayanan, Edmund M. Clarke	Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems.	FMCAD	2010	DBLP BibTeX RDF
1	Edmund M. Clarke, Andrei Voronkov (eds.)	Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers	LPAR (Dakar)	2010	DBLP DOI BibTeX RDF
1	William Klieber, Samir Sapra, Sicun Gao, Edmund M. Clarke	A Non-prenex, Non-clausal QBF Solver with Game-State Learning.	SAT	2010	DBLP DOI BibTeX RDF
1	Håkan L. S. Younes, Edmund M. Clarke, Paolo Zuliani	Statistical Verification of Probabilistic Properties with Unbounded Until.	SBMF	2010	DBLP DOI BibTeX RDF
1	Haijun Gong, Paolo Zuliani, Anvesh Komuravelli, James R. Faeder, Edmund M. Clarke	Computational Modeling and Verification of Signaling Pathways in Cancer.	ANB	2010	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Robert P. Kurshan, Helmut Veith	The Localization Reduction and Counterexample-Guided Abstraction Refinement.	Essays in Memory of Amir Pnueli	2010	DBLP DOI BibTeX RDF
1	Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang	Automated Assume-Guarantee Reasoning through Implicit Learning.	CAV	2010	DBLP DOI BibTeX RDF
1	Paolo Zuliani, André Platzer, Edmund M. Clarke	Bayesian statistical model checking with application to Simulink/Stateflow verification.	HSCC	2010	DBLP DOI BibTeX RDF	bayesian statis tics, statistical model checking, hybrid systems, probabilistic model checking, stochastic systems
1	Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Fei He, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang, Lei Zhu	Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning.	ISoLA	2010	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, E. Allen Emerson, Joseph Sifakis	Model checking: algorithmic verification and debugging.	Commun. ACM	2009	DBLP DOI BibTeX RDF
1	Anmol Mathur, Masahiro Fujita, Edmund M. Clarke, Pascal Urard	Functional Equivalence Verification Tools in High-Level Synthesis Flows.	IEEE Design & Test of Computers	2009	DBLP DOI BibTeX RDF
1	Himanshu Jain, Edmund M. Clarke, Orna Grumberg	Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations.	Formal Methods in System Design	2009	DBLP DOI BibTeX RDF
1	André Platzer, Edmund M. Clarke	Computing differential invariants of hybrid systems as fixedpoints.	Formal Methods in System Design	2009	DBLP DOI BibTeX RDF
1	Yu-Fang Chen, Azadeh Farzan, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang	Learning Minimal Separating DFA's for Compositional Verification.	TACAS	2009	DBLP DOI BibTeX RDF
1	Himanshu Jain, Edmund M. Clarke	Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts.	DAC	2009	DBLP DOI BibTeX RDF	NNF, verification, Boolean satisfiability, DPLL
1	Sumit Kumar Jha, Edmund M. Clarke, Christopher James Langmead, Axel Legay, André Platzer, Paolo Zuliani	A Bayesian Approach to Model Checking Biological Systems.	CMSB	2009	DBLP DOI BibTeX RDF
1	André Platzer, Edmund M. Clarke	Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study.	FM	2009	DBLP DOI BibTeX RDF
1	Edmund M. Clarke	My 27-year Quest to Overcome the State Explosion Problem.	LICS	2009	DBLP DOI BibTeX RDF
1	Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke	Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.	IEEE Trans. on CAD of Integrated Circuits and Systems	2008	DBLP DOI BibTeX RDF
1	Sagar Chaki, Edmund M. Clarke, Natasha Sharygina, Nishant Sinha	Verification of evolving software via component substitutability analysis.	Formal Methods in System Design	2008	DBLP DOI BibTeX RDF	Automata learning, Software engineering, Model checking, Predicate abstraction, Compositional verification, Assume-guarantee reasoning
1	Azadeh Farzan, Yu-Fang Chen, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang	Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages.	TACAS	2008	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Muralidhar Talupur, Helmut Veith	Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems.	TACAS	2008	DBLP DOI BibTeX RDF
1	Edmund M. Clarke	Model Checking - My 27-Year Quest to Overcome the State Explosion Problem.	LPAR	2008	DBLP DOI BibTeX RDF
1	Edmund M. Clarke	The Birth of Model Checking.	25 Years of Model Checking	2008	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, E. Allen Emerson	Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic.	25 Years of Model Checking	2008	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, James R. Faeder, Christopher James Langmead, Leonard A. Harris, Sumit Kumar Jha, Axel Legay	Statistical Model Checking in BioLab: Applications to the Automated Analysis of T-Cell Receptor Signaling Pathway.	CMSB	2008	DBLP DOI BibTeX RDF
1	Himanshu Jain, Edmund M. Clarke, Orna Grumberg	Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations.	CAV	2008	DBLP DOI BibTeX RDF
1	André Platzer, Edmund M. Clarke	Computing Differential Invariants of Hybrid Systems as Fixedpoints.	CAV	2008	DBLP DOI BibTeX RDF	verification of hybrid systems, verification logic, fixedpoint engine, differential invariants
1	Flavio Lerda, James Kapinski, Edmund M. Clarke, Bruce H. Krogh	Verification of Supervisory Control Software Using State Proximity and Merging.	HSCC	2008	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Alexandre Donzé, Axel Legay	Statistical Model Checking of Mixed-Analog Circuits with an Application to a Third Order Delta-Sigma Modulator.	Haifa Verification Conference	2008	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Flavio Lerda	Model Checking: Software and Beyond.	J. UCS	2007	DBLP BibTeX RDF
1	Edmund M. Clarke, Himanshu Jain, Daniel Kroening	Verification of SpecC using predicate abstraction.	Formal Methods in System Design	2007	DBLP DOI BibTeX RDF	Verification, System level design, Predicate abstraction
1	Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke	VCEGAR: Verilog CounterExample Guided Abstraction Refinement.	TACAS	2007	DBLP DOI BibTeX RDF
1	Nishant Sinha, Edmund M. Clarke	SAT-Based Compositional Verification Using Lazy Learning.	CAV	2007	DBLP DOI BibTeX RDF
1	André Platzer, Edmund M. Clarke	The Image Computation Problem in Hybrid Systems Model Checking.	HSCC	2007	DBLP DOI BibTeX RDF	model checking, hybrid systems, image computation
1	Sumit Kumar Jha, Bruce H. Krogh, James E. Weimer, Edmund M. Clarke	Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction.	HSCC	2007	DBLP DOI BibTeX RDF
1	Stephen Magill, Josh Berdine, Edmund M. Clarke, Byron Cook	Arithmetic Strengthening for Shape Analysis.	SAS	2007	DBLP DOI BibTeX RDF
1	Sagar Chaki, Edmund M. Clarke, Nicholas Kidd, Thomas W. Reps, Tayssir Touili	Verifying Concurrent Message-Passing C Programs with Recursive Calls.	TACAS	2006	DBLP DOI BibTeX RDF
1	Himanshu Jain, Constantinos Bartzis, Edmund M. Clarke	Satisfiability Checking of Non-clausal Formulas Using General Matings.	SAT	2006	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Marius Minea, Ferucio Laurentiu Tiplea (eds.)	Verification of Infinite-State Systems with Applications to Security, Proceedings of the NATO Advanced Research Workshop "Verification of Infinite State Systems with Applications to Security VISSAS 2005", Timisoara, Romania, March 17-22, 2005	VISSAS	2006	DBLP BibTeX RDF
1	Vaibhav Mehta, Constantinos Bartzis, Haifeng Zhu, Edmund M. Clarke, Jeannette M. Wing	Ranking Attack Graphs.	RAID	2006	DBLP DOI BibTeX RDF	Google PageRank, Model Checking, security metric, Attack Graph, Attack Model
1	Edmund M. Clarke, Muralidhar Talupur, Helmut Veith	Environment Abstraction for Parameterized Verification.	VMCAI	2006	DBLP DOI BibTeX RDF
1	Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha	Concurrent software verification with states, events, and deadlocks.	Formal Asp. Comput.	2005	DBLP DOI BibTeX RDF	Concurrent software, States and events, Counterexample-guided abstraction refinement, Model checking, Temporal logic, Deadlock, Compositional reasoning
1	Sagar Chaki, Edmund M. Clarke, Somesh Jha, Helmut Veith	An Iterative Framework for Simulation Conformance.	J. Log. Comput.	2005	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman	Computational challenges in bounded model checking.	STTT	2005	DBLP DOI BibTeX RDF	Bonded-Model-checking, Completeness-Threshold, Complexity
1	Edmund M. Clarke, Ansgar Fehnker, Sumit Kumar Jha, Helmut Veith	Temporal Logic Model Checking.	Handbook of Networked and Embedded Control Systems	2005	DBLP BibTeX RDF
1	Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav	SATABS: SAT-Based Predicate Abstraction for ANSI-C.	TACAS	2005	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Natasha Sharygina, Nishant Sinha	Program Compatibility Approaches.	FMCO	2005	DBLP DOI BibTeX RDF
1	Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke	Word level predicate abstraction and refinement for verifying RTL verilog.	DAC	2005	DBLP DOI BibTeX RDF	SAT, predicate abstraction, verilog
1	Sagar Chaki, Edmund M. Clarke, Orna Grumberg, Joël Ouaknine, Natasha Sharygina, Tayssir Touili, Helmut Veith	State/Event Software Verification for Branching-Time Specifications.	IFM	2005	DBLP DOI BibTeX RDF	Concurrent Software Model Checking, State/Event-based Verification, Branching-time Temporal Logic, Automated Abstraction Refinement
1	Edmund M. Clarke, Anubhav Gupta, Himanshu Jain, Helmut Veith	Model Checking: Back and Forth between Hardware and Software.	VSTTE	2005	DBLP DOI BibTeX RDF
1	Natasha Sharygina, Sagar Chaki, Edmund M. Clarke, Nishant Sinha	Dynamic Component Substitutability Analysis.	FM	2005	DBLP DOI BibTeX RDF	Verification of Evolving Software, Learning Regular Sets, Assume/Guarantee Reasoning, Software Model Checking
1	Edmund M. Clarke, Himanshu Jain, Nishant Sinha	Grand Challenge: Model Check Software.	VISSAS	2005	DBLP BibTeX RDF
1	Sagar Chaki, Edmund M. Clarke, Nishant Sinha, Prasanna Thati	Automated Assume-Guarantee Reasoning for Simulation Conformance.	CAV	2005	DBLP DOI BibTeX RDF
1	Ansgar Fehnker, Edmund M. Clarke, Sumit Kumar Jha, Bruce H. Krogh	Refining Abstractions of Hybrid Systems Using Counterexample Fragments.	HSCC	2005	DBLP DOI BibTeX RDF
1	Anubhav Gupta, Edmund M. Clarke	Reconsidering CEGAR: Learning Good Abstractions without Refinement.	ICCD	2005	DBLP DOI BibTeX RDF
1	Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, Helmut Veith	Modular Verification of Software Components in C.	IEEE Trans. Software Eng.	2004	DBLP DOI BibTeX RDF
1	Edjard Mota, Edmund M. Clarke, Alex Groce, Waleska Oliveira, Marcia Falcão, Jorge Kanda	VeriAgent: an Approach to Integrating UML and Formal Verification Tools.	Electr. Notes Theor. Comput. Sci.	2004	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Anubhav Gupta, Ofer Strichman	SAT-based counterexample-guided abstraction refinement.	IEEE Trans. on CAD of Integrated Circuits and Systems	2004	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav	Predicate Abstraction of ANSI-C Programs Using SAT.	Formal Methods in System Design	2004	DBLP DOI BibTeX RDF	ANSI-C, SAT, predicate abstraction
1	Sagar Chaki, Edmund M. Clarke, Alex Groce, Joël Ouaknine, Ofer Strichman, Karen Yorav	Efficient Verification of Sequential and Concurrent C Programs.	Formal Methods in System Design	2004	DBLP DOI BibTeX RDF	concurrency, process algebra, software verification, predicate abstraction, abstraction refinement
1	Edmund M. Clarke, Muralidhar Talupur, Tayssir Touili, Helmut Veith	Verification by Network Decomposition.	CONCUR	2004	DBLP DOI BibTeX RDF
1	Daniel Kroening, Alex Groce, Edmund M. Clarke	Counterexample Guided Abstraction Refinement Via Program Execution.	ICFEM	2004	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Daniel Kroening	Tutorial: Software Model Checking.	ICFEM	2004	DBLP DOI BibTeX RDF
1	Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina	Automated, compositional and iterative deadlock detection.	MEMOCODE	2004	DBLP DOI BibTeX RDF
1	Himanshu Jain, Daniel Kroening, Edmund M. Clarke	Verification of SpecC using predicate abstraction.	MEMOCODE	2004	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Daniel Kroening, Flavio Lerda	A Tool for Checking ANSI-C Programs.	TACAS	2004	DBLP DOI BibTeX RDF
1	Pankaj Chauhan, Edmund M. Clarke, Daniel Kroening	A SAT-based algorithm for reparameterization in symbolic simulation.	DAC	2004	DBLP DOI BibTeX RDF	SAT checkers, safety property checking, bounded model checking, symbolic simulation, parametric representation
1	Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha	State/Event-Based Software Model Checking.	IFM	2004	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman	Completeness and Complexity of Bounded Model Checking.	VMCAI	2004	DBLP DOI BibTeX RDF
1	Daniel Kroening, Edmund M. Clarke	Checking consistency of C and Verilog using predicate abstraction and induction.	ICCAD	2004	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Ansgar Fehnker, Zhi Han, Bruce H. Krogh, Joël Ouaknine, Olaf Stursberg, Michael Theobald	Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems.	Int. J. Found. Comput. Sci.	2003	DBLP DOI BibTeX RDF
1	Sagar Chaki, Joël Ouaknine, Karen Yorav, Edmund M. Clarke	Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach.	Electr. Notes Theor. Comput. Sci.	2003	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith	Counterexample-guided abstraction refinement for symbolic model checking.	J. ACM	2003	DBLP DOI BibTeX RDF	temporal logic, Abstraction, symbolic model checking, hardware verification
1	Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero	Efficient verification of security protocols using partial-order reductions.	STTT	2003	DBLP DOI BibTeX RDF	Model checking, Security protocols, Partial-order reduction
1	Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, Yunshan Zhu	Bounded model checking.	Advances in Computers	2003	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang	High Level Verification of Control Intensive Systems Using Predicate Abstraction.	MEMOCODE	2003	DBLP DOI BibTeX RDF
1	Edmund M. Clarke	SAT-Based Counterexample Guided Abstraction Refinement in Model Checking.	CADE	2003	DBLP DOI BibTeX RDF
1	Edmund M. Clarke	Counterexample-Guided Abstraction Refinement. (PDF / PS)	TIME	2003	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Ansgar Fehnker, Zhi Han, Bruce H. Krogh, Olaf Stursberg, Michael Theobald	Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement.	TACAS	2003	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Muralidhar Talupur, Helmut Veith, Dong Wang	SAT Based Predicate Abstraction for Hardware Verification.	SAT	2003	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Masahiro Fujita, David P. Gluch	Model Checking for Dependable Software-Intensive Systems. (PDF / PS)	DSN	2003	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Daniel Kroening, Karen Yorav	Behavioral consistency of C and verilog programs using bounded model checking.	DAC	2003	DBLP DOI BibTeX RDF	ANSI-C, equivalence checking, verilog
1	Sagar Chaki, Edmund M. Clarke, Alex Groce, Ofer Strichman	Predicate Abstraction with Minimum Predicates.	CHARME	2003	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Helmut Veith	Counterexamples Revisited: Principles, Algorithms, Applications.	Verification: Theory and Practice	2003	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang	Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates.	CAV	2003	DBLP DOI BibTeX RDF
1	Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, Helmut Veith	Modular Verification of Software Components in C. (PDF / PS)	ICSE	2003	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Daniel Kroening, Karen Yorav	Specifying and Verifying Systems with Multiple Clocks.	ICCD	2003	DBLP DOI BibTeX RDF
1	Samir Sapra, Michael Theobald, Edmund M. Clarke	SAT-Based Algorithms for Logic Minimization.	ICCD	2003	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Masahiro Fujita, Sreeranga P. Rajan, Thomas W. Reps, Subash Shankar, Tim Teitelbaum	Program slicing for VHDL.	STTT	2002	DBLP DOI BibTeX RDF	Model checking, Formal verification, VHDL, Program slicing, Hardware description languages

Publications of "Edmund M. Clarke" ( http://dblp.L3S.de/Authors/Edmund_M._Clarke )