Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
10 | John Whaley, Monica S. Lam |
Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. |
PLDI |
2004 |
DBLP DOI BibTeX RDF |
inclusion-based, Java, scalable, logic programming, program analysis, Datalog, binary decision diagrams, cloning, pointer analysis, context-sensitive |
10 | Nicole Drechsler, Mario Hilgemeier, Görschwin Fey, Rolf Drechsler |
Disjoint Sum of Product Minimization by Evolutionary Algorithms. |
EvoWorkshops |
2004 |
DBLP DOI BibTeX RDF |
|
10 | Klaus Schneider 0001, Jens Brandt 0001, Tobias Schüle |
Causality analysis of synchronous programs with delayed actions. |
CASES |
2004 |
DBLP DOI BibTeX RDF |
causality, synchronous languages, ternary logic, fixpoints |
10 | Zijiang Yang 0006, Rajeev Alur |
Variable Reuse for Efficient Image Computation. |
FMCAD |
2004 |
DBLP DOI BibTeX RDF |
|
10 | Mohammad Awedh, Fabio Somenzi |
Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States. |
FMCAD |
2004 |
DBLP DOI BibTeX RDF |
|
10 | Orna Grumberg, Assaf Schuster, Avi Yadgar |
Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis. |
FMCAD |
2004 |
DBLP DOI BibTeX RDF |
|
10 | Masahito Kurihara, Hisashi Kondo |
Efficient BDD Encodings for Partial Order Constraints with Application to Expert Systems in Software Verification. |
IEA/AIE |
2004 |
DBLP DOI BibTeX RDF |
|
10 | Jie-Hong Roland Jiang, Robert K. Brayton |
On the verification of sequential equivalence. |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. |
2003 |
DBLP DOI BibTeX RDF |
|
10 | Tuba Yavuz-Kahveci, Tevfik Bultan |
A symbolic manipulator for automated verification of reactive systems with heterogeneous data types. |
Int. J. Softw. Tools Technol. Transf. |
2003 |
DBLP DOI BibTeX RDF |
Composite representation, BDD, Symbolic model checking, Presburger arithmetic |
10 | Poul Frederick Williams, Henrik Reif Andersen, Henrik Hulgaard |
Satisfiability checking using Boolean Expression Diagrams. |
Int. J. Softw. Tools Technol. Transf. |
2003 |
DBLP DOI BibTeX RDF |
|
10 | Juraj Hromkovic, Martin Sauerhoff |
The Power of Nondeterminism and Randomness for Oblivious Branching Programs. |
Theory Comput. Syst. |
2003 |
DBLP DOI BibTeX RDF |
|
10 | Dirk Beyer 0001, Claus Lewerentz, Andreas Noack |
Rabbit: A Tool for BDD-Based Verification of Real-Time Systems. |
CAV |
2003 |
DBLP DOI BibTeX RDF |
|
10 | Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook |
A Symbolic Approach to Predicate Abstraction. |
CAV |
2003 |
DBLP DOI BibTeX RDF |
|
10 | Sanjit A. Seshia, Randal E. Bryant |
Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods. |
CAV |
2003 |
DBLP DOI BibTeX RDF |
|
10 | Ateet Bhalla, Inês Lynce, José T. de Sousa, João Marques-Silva 0001 |
Heuristic Backtracking Algorithms for SAT. |
MTV |
2003 |
DBLP DOI BibTeX RDF |
|
10 | Gianpiero Cabodi, Sergio Nocco, Stefano Quer |
Improving SAT-Based Bounded Model Checking by Means of BDD-Based Approximate Traversals. |
DATE |
2003 |
DBLP DOI BibTeX RDF |
|
10 | P. W. Chandana Prasad, M. Maria Dominic, Ashutosh Kumar Singh |
Variable Order Verification Use of Logic Representation. |
ICADL |
2003 |
DBLP DOI BibTeX RDF |
|
10 | Junhao Shi, Görschwin Fey, Rolf Drechsler |
BDD Based Synthesis of Symmetric Functions with Full Path-Delay Fault Testability. |
Asian Test Symposium |
2003 |
DBLP DOI BibTeX RDF |
|
10 | Akihiko Tozawa, Masami Hagiya |
XML Schema Containment Checking Based on Semi-implicit Techniques. |
CIAA |
2003 |
DBLP DOI BibTeX RDF |
|
10 | E. Allen Emerson, Thomas Wahl |
On Combining Symmetry Reduction and Symbolic Representation for Efficient Model Checking. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
10 | Rachel Tzoref, Mark Matusevich, Eli Berger, Ilan Beer |
An Optimized Symbolic Bounded Model Checking Engine. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
10 | Enric Pastor, Marco A. Peña |
Efficient Hybrid Reachability Analysis for Asynchronous Concurrent Systems. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
10 | Rüdiger Ebendt |
Reducing the number of variable movements in exact BDD minimization. |
ISCAS (5) |
2003 |
DBLP DOI BibTeX RDF |
|
10 | Bijan Alizadeh, Mohammad Reza Kakoee |
Using Integer Equations for High Level Formal Verification Property Checking. |
ISQED |
2003 |
DBLP DOI BibTeX RDF |
|
10 | 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 |
10 | Amit Goel, Gagan Hasteer, Randal E. Bryant |
Symbolic representation with ordered function templates. |
DAC |
2003 |
DBLP DOI BibTeX RDF |
function templates, logic design verification, boolean functions, binary decision diagrams, symbolic simulation |
10 | David Déharbe, Silvio Ranise |
Light-Weight Theorem Proving for Debugging and Verifying Units of Code. |
SEFM |
2003 |
DBLP DOI BibTeX RDF |
|
10 | Shin-ichi Minato |
Streaming BDD Manipulation. |
IEEE Trans. Computers |
2002 |
DBLP DOI BibTeX RDF |
algorithm, verification, testing, data structure, logic design, binary decision diagram, BDD, combinatorial problem, VLSI CAD |
10 | William N. N. Hung, Xiaoyu Song, El Mostapha Aboulhamid, Michael A. Driscoll |
BDD minimization by scatter search. |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. |
2002 |
DBLP DOI BibTeX RDF |
|
10 | Guoqiang Pan, Ulrike Sattler, Moshe Y. Vardi |
BDD-Based Decision Procedures for K. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
10 | Hee-Hwan Kwak, In-Ho Moon, James H. Kukula, Thomas R. Shiple |
Combinational equivalence checking through function transformation. |
ICCAD |
2002 |
DBLP DOI BibTeX RDF |
combinational verification, equivalence checking |
10 | Tuba Yavuz-Kahveci, Tevfik Bultan |
Automated Verification of Concurrent Linked Lists with Counters. |
SAS |
2002 |
DBLP DOI BibTeX RDF |
|
10 | Geun Rae Cho, Tom Chen 0001 |
Mixed PTL/Static Logic Synthesis Using Genetic Algorithms for Low-Power Applications. |
ISQED |
2002 |
DBLP DOI BibTeX RDF |
Mixed PTL/Static, Lower-Power Technology Mapping, Logic Synthesis, Pass Transistor Logic |
10 | Marc Solé, Enric Pastor |
Traversal Techniques for Concurrent Systems. |
FMCAD |
2002 |
DBLP DOI BibTeX RDF |
|
10 | Torsten Robschink, Gregor Snelting |
Efficient path conditions in dependence graphs. |
ICSE |
2002 |
DBLP DOI BibTeX RDF |
|
10 | Malay K. Ganai, Adnan Aziz |
Improved SAT-Based Bounded Reachability Analysis. |
ASP-DAC/VLSI Design |
2002 |
DBLP DOI BibTeX RDF |
|
10 | Ian Davies, William J. Knottenbelt, Pieter S. Kritzinger |
Symbolic Methods for the State Space Exploration of GSPN Models. |
Computer Performance Evaluation / TOOLS |
2002 |
DBLP DOI BibTeX RDF |
|
10 | Alessandro Cimatti, Enrico Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella |
Integrating BDD-Based and SAT-Based Symbolic Model Checking. |
FroCoS |
2002 |
DBLP DOI BibTeX RDF |
|
10 | Randal E. Bryant, Steven M. German, Miroslav N. Velev |
Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. |
ACM Trans. Comput. Log. |
2001 |
DBLP DOI BibTeX RDF |
processor verfication, decision procedures, uninterpreted functions |
10 | Enric Pastor, Jordi Cortadella, Oriol Roig |
Symbolic Analysis of Bounded Petri Nets. |
IEEE Trans. Computers |
2001 |
DBLP DOI BibTeX RDF |
Binary Decition Diagrams, Petri nets, formal verification, symbolic methods |
10 | Rolf Drechsler, Wolfgang Günther 0001, Fabio Somenzi |
Using lower bounds during dynamic BDD minimization. |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. |
2001 |
DBLP DOI BibTeX RDF |
|
10 | Malay K. Ganai, Praveen Yalagandula, Adnan Aziz, Andreas Kuehlmann, Vigyan Singhal |
SIVA: A System for Coverage-Directed State Space Search. |
J. Electron. Test. |
2001 |
DBLP DOI BibTeX RDF |
formal methods, coverage, functional verification, guided search |
10 | Thomas Ball, Sriram K. Rajamani |
Bebop: a path-sensitive interprocedural dataflow engine. |
PASTE |
2001 |
DBLP DOI BibTeX RDF |
|
10 | Javier Esparza, Stefan Schwoon |
A BDD-Based Model Checker for Recursive Programs. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
10 | John Moondanos, Carl-Johan H. Seger, Ziyad Hanna, Daher Kaiss |
CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
10 | Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu 0004, Helmut Veith |
Progress on the State Explosion Problem in Model Checking. |
Informatics |
2001 |
DBLP DOI BibTeX RDF |
|
10 | Per Lindgren, Mikael Kerttu, Mitchell A. Thornton, Rolf Drechsler |
Low power optimization technique for BDD mapped circuits. |
ASP-DAC |
2001 |
DBLP DOI BibTeX RDF |
|
10 | Michael Baldamus, Klaus Schneider 0001 |
The BDD Space Complexity of Different Forms of Concurrency. |
ACSD |
2001 |
DBLP DOI BibTeX RDF |
|
10 | Pankaj Chauhan, Edmund M. Clarke, Somesh Jha, James H. Kukula, Helmut Veith, Dong Wang |
Using Combinatorial Optimization Methods for Quantification Scheduling. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
10 | Tuba Yavuz-Kahveci, Murat Tuncer, Tevfik Bultan |
A Library for Composite Symbolic Representations. |
TACAS |
2001 |
DBLP DOI BibTeX RDF |
|
10 | Poul Frederick Williams, Henrik Reif Andersen, Henrik Hulgaard |
Satisfiability Checking Using Boolean Expression Diagrams. |
TACAS |
2001 |
DBLP DOI BibTeX RDF |
|
10 | S. Sriram, R. Tandon, Pallab Dasgupta, P. P. Chakrabarti 0001 |
Symbolic verification of Boolean constraints over partially specified functions. |
ISCAS (5) |
2001 |
DBLP DOI BibTeX RDF |
|
10 | Nicole Drechsler, Frank Schmiedle, Daniel Große, Rolf Drechsler |
Heuristic Learning Based on Genetic Programming. |
EuroGP |
2001 |
DBLP DOI BibTeX RDF |
|
10 | Wolfgang Günther 0001, Rolf Drechsler |
Performance Driven Optimization for MUX based FPGAs. |
VLSI Design |
2001 |
DBLP DOI BibTeX RDF |
|
10 | David E. Long, Mahesh A. Iyer, Miron Abramovici |
FILL and FUNI: algorithms to identify illegal states and sequentially untestable faults. |
ACM Trans. Design Autom. Electr. Syst. |
2000 |
DBLP DOI BibTeX RDF |
illegal states, sequential circuits, automatic test generation, untestable faults |
10 | Priyank Kalla, Zhihong Zeng, Maciej J. Ciesielski, ChiLai Huang |
A BDD-Based Satisfiability Infrastructure Using the Unate Recursive Paradigm. |
DATE |
2000 |
DBLP DOI BibTeX RDF |
|
10 | Steffen Hölldobler, Hans-Peter Störr |
Solving the Entailment Problem in the Fluent Calculus Using Binary Decision Diagrams. |
Computational Logic |
2000 |
DBLP DOI BibTeX RDF |
|
10 | Dragan Jankovic, Wolfgang Günther 0001, Rolf Drechsler |
Lower Bound Sifting for MDDs. |
ISMVL |
2000 |
DBLP DOI BibTeX RDF |
|
10 | Wolfgang Günther 0001, Nicole Drechsler, Rolf Drechsler, Bernd Becker 0001 |
Verification of Designs Containing Black Boxes. |
EUROMICRO |
2000 |
DBLP DOI BibTeX RDF |
|
10 | Rolf Drechsler, Wolfgang Günther 0001, Bernd Becker 0001 |
Testability of Circuits Derived from Lattice Diagrams. |
EUROMICRO |
2000 |
DBLP DOI BibTeX RDF |
|
10 | Wolfgang Günther 0001, Rolf Drechsler, Stefan Höreth |
Efficient Dynamic Minimization of Word-Level DDs Based on Lower Bound Computation. |
ICCD |
2000 |
DBLP DOI BibTeX RDF |
|
10 | In-Ho Moon, Gary D. Hachtel, Fabio Somenzi |
Border-Block Triangular Form and Conjunction Schedule in Image Computation. |
FMCAD |
2000 |
DBLP DOI BibTeX RDF |
|
10 | Randal E. Bryant, Pankaj Chauhan, Edmund M. Clarke, Amit Goel |
A Theory of Consistency for Modular Synchronous Systems. |
FMCAD |
2000 |
DBLP DOI BibTeX RDF |
|
10 | Aarti Gupta, Pranav Ashar |
Fast Error Diagnosis for Combinational Verification. |
VLSI Design |
2000 |
DBLP DOI BibTeX RDF |
Satisfiability Checking, Formal Verification, Combinational Circuits, Binary Decision Diagrams, Logic Simulation, Error Diagnosis |
10 | Congguang Yang, Maciej J. Ciesielski, Vigyan Singhal |
BDS: a BDD-based logic optimization system. |
DAC |
2000 |
DBLP DOI BibTeX RDF |
|
10 | Chris Wilson, David L. Dill |
Reliable verification using symbolic simulation with scalar values. |
DAC |
2000 |
DBLP DOI BibTeX RDF |
|
10 | Roderick Bloem, Kavita Ravi, Fabio Somenzi |
Symbolic guided search for CTL model checking. |
DAC |
2000 |
DBLP DOI BibTeX RDF |
|
10 | Dinos Moundanos, Jacob A. Abraham |
On Design Validation Using Verification Technology. |
J. Electron. Test. |
1999 |
DBLP DOI BibTeX RDF |
extracted control flow machine, verification, abstraction, test generation, coverage analysis, OBDDs |
10 | Enrique San Millán, Luis Entrena, José Alberto Espejo, Silvia Chiusano, Fulvio Corno |
Integrating Symbolic Techniques in ATPG-Based Sequential Logic Optimization. |
DATE |
1999 |
DBLP DOI BibTeX RDF |
|
10 | Miroslav N. Velev, Randal E. Bryant |
Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
10 | Y. Tachi, Satoshi Yamane |
Real-Time Symbolic Model Checking for Hard Real-Time Systems. |
RTCSA |
1999 |
DBLP DOI BibTeX RDF |
real-time symbolic model checking, real-time systems, timed automaton, real-time temporal logic |
10 | Laurent Mauborgne |
Binary Decision Graphs. |
SAS |
1999 |
DBLP DOI BibTeX RDF |
|
10 | Hafiz Md. Hasan Babu, Tsutomu Sasao |
Shared Multiple-Valued Decision Diagrams for Multiple-Output Functions. |
ISMVL |
1999 |
DBLP DOI BibTeX RDF |
|
10 | Andreas G. Veneris, Ibrahim N. Hajj |
Correcting multiple design errors in digital VLSI circuits. |
ISCAS (1) |
1999 |
DBLP DOI BibTeX RDF |
|
10 | Samuel Devulder, Jean-Luc Lambert |
A Comparative Study between Linear Programming Validation (LPV) and other Verification Methods. |
ASE |
1999 |
DBLP DOI BibTeX RDF |
|
10 | Jesper B. Møller, Jakob Lichtenberg, Henrik Reif Andersen, Henrik Hulgaard |
Difference Decision Diagrams. |
CSL |
1999 |
DBLP DOI BibTeX RDF |
|
10 | Robert A. Thacker, Wendy Belluomini, Chris J. Myers |
Timed Circuit Synthesis Using Implicit Methods. |
VLSI Design |
1999 |
DBLP DOI BibTeX RDF |
|
10 | Gi-Joon Nam, Karem A. Sakallah, Rob A. Rutenbar |
Satisfiability-Based Detailed FPGA Routing. |
VLSI Design |
1999 |
DBLP DOI BibTeX RDF |
|
10 | Pankaj Chauhan, Pallab Dasgupta, P. P. Chakrabarti 0001 |
Exploiting Isomorphism for Compaction and Faster Simulation of Binary Decision Diagrams. |
VLSI Design |
1999 |
DBLP DOI BibTeX RDF |
|
10 | Detlef Sieling |
Lower Bounds for Linear Transformed OBDDs and FBDDs (Extende Abstract). |
FSTTCS |
1999 |
DBLP DOI BibTeX RDF |
|
10 | Fabrizio Ferrandi, Franco Fummi, Enrico Macii, Massimo Poncino |
Power Estimation of Behavioral Descriptions. |
DATE |
1998 |
DBLP DOI BibTeX RDF |
Behavioral power estimation, macromodeling, design exploration |
10 | Kazuhiro Nakamura, Satoshi Yamane |
Formal Verification of Real-Time Software by Symbolic Model-Checker. |
ACSD |
1998 |
DBLP DOI BibTeX RDF |
temporal logic, approximations, BDD, symbolic model-checking, real-time software |
10 | Edmund M. Clarke, Sergey Berezin |
Model Checking: Historical Perspective and Example (Extended Abstract). |
TABLEAUX |
1998 |
DBLP DOI BibTeX RDF |
|
10 | Tevfik Bultan, Richard Gerber 0001, Christopher League |
Verifying Systems with Integer Constraints and Boolean Predicates: A Composite Approach. |
ISSTA |
1998 |
DBLP DOI BibTeX RDF |
|
10 | David James Sherman, Nicolas Magnier |
Factotum: Automatic and Systematic Sharing Support for Systems Analyzers. |
TACAS |
1998 |
DBLP DOI BibTeX RDF |
|
10 | Jürgen Ruf, Thomas Kropf |
Using MTBDDs for Compostion and Model Checking of Real-Time Systems. |
FMCAD |
1998 |
DBLP DOI BibTeX RDF |
|
10 | Yufeng Luo, Tjahjadi Wongsonegoro, Adnan Aziz |
Hybrid Techniques for Fast Functional Simulation. |
DAC |
1998 |
DBLP DOI BibTeX RDF |
ASIC verification, simulation, emulation |
10 | Timothy Kam, Tiziano Villa, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
Implicit computation of compatible sets for state minimization of ISFSMs. |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. |
1997 |
DBLP DOI BibTeX RDF |
|
10 | Bard Bloom, Allan Cheng, Ashvin Dsouza |
Using a Protean Language to Enhance Expressiveness in Specification. |
IEEE Trans. Software Eng. |
1997 |
DBLP DOI BibTeX RDF |
model checking, verification, Formal methods, specification, process algebra, structured operational semantics |
10 | William Chan 0001, Richard J. Anderson, Paul Beame, David Notkin |
Combining Constraint Solving and Symbolic Model Checking for a Class of a Systems with Non-linear Constraints. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
10 | Rajeev Alur, Robert K. Brayton, Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani |
Partial-Order Reduction in Symbolic State Space Exploration. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
10 | Hoon Choi, Seung Ho Hwang |
Improving the accuracy of support-set finding method for power estimation of combinational circuits. |
ED&TC |
1997 |
DBLP DOI BibTeX RDF |
|
10 | Aiguo Xie, Peter A. Beerel |
Symbolic Techniques for Performance Analysis of Timed Systems Based on Average Time Separation of Events. |
ASYNC |
1997 |
DBLP DOI BibTeX RDF |
time separation of events, Markov chains, probabilistic modeling, asynchronous, performance metrics, sojourn times, timed systems, symbolic techniques |
10 | Christel Baier, Edmund M. Clarke, Vasiliki Hartonas-Garmhausen, Marta Z. Kwiatkowska, Mark Ryan 0001 |
Symbolic Model Checking for Probabilistic Processes. |
ICALP |
1997 |
DBLP DOI BibTeX RDF |
|
10 | Silvia Chiusano, Fulvio Corno, Paolo Prinetto, Maurizio Rebaudengo, Matteo Sonza Reorda |
Guaranteeing Testability in Re-encoding for Low Power. |
Asian Test Symposium |
1997 |
DBLP DOI BibTeX RDF |
Initialization sequence, Genetic Algorithm, ATPG |
10 | Christoph Scholl 0001, Rolf Drechsler, Bernd Becker 0001 |
Functional simulation using binary decision diagrams. |
ICCAD |
1997 |
DBLP DOI BibTeX RDF |
Binary Decision Diagrams, Functional simulation |
10 | Sreeranga P. Rajan, Natarajan Shankar, Mandayam K. Srivas |
Industrial Strength Formal Verification Techniques for Hardware Designs. |
VLSI Design |
1997 |
DBLP DOI BibTeX RDF |
|
10 | Bwolen Yang, David R. O'Hallaron |
Parallel Breadth-First BDD Construction. |
PPoPP |
1997 |
DBLP DOI BibTeX RDF |
|
10 | Krzysztof Bilinski, Erik L. Dagless |
High Level Synthesis of Synchronous Parallel Controllers. |
Application and Theory of Petri Nets |
1996 |
DBLP DOI BibTeX RDF |
|
10 | Rosario Pugliese, Enrico Tronci |
Automatic Verification of a Hydroelectric Power Plant. |
FME |
1996 |
DBLP DOI BibTeX RDF |
|