Article

BDD Based Procedures for a Theory of Equality with Uninterpreted Functions

Authors:

Vigyan SinghalAuthors Info & Claims

CAV '98: Proceedings of the 10th International Conference on Computer Aided Verification

Pages 244 - 255

Published: 28 June 1998 Publication History

Abstract

No abstract available.

Cited By

View all

Velev MGao P(2011)Automatic formal verification of reconfigurable DSPsProceedings of the 16th Asia and South Pacific Design Automation Conference10.5555/1950815.1950881(293-296)Online publication date: 25-Jan-2011
https://dl.acm.org/doi/10.5555/1950815.1950881
Velev MGao P(2010)Method for formal verification of soft-error tolerance mechanisms in pipelined microprocessorsProceedings of the 12th international conference on Formal engineering methods and software engineering10.5555/1939864.1939894(355-370)Online publication date: 17-Nov-2010
https://dl.acm.org/doi/10.5555/1939864.1939894
Velev MGao PLin Y(2010)A method for debugging of pipelined processors in formal verification by correspondence checkingProceedings of the 2010 Asia and South Pacific Design Automation Conference10.5555/1899721.1899866(619-624)Online publication date: 18-Jan-2010
https://dl.acm.org/doi/10.5555/1899721.1899866
Show More Cited By

Recommendations

BDD Based Procedures for a Theory of Equality with Uninterpreted Functions

The logic of equality with uninterpreted functions has been proposed for verifying abstract hardware designs. The ability to perform fast satisfiability checking over this logic is imperative for such verification paradigms to be successful. We present ...
Commutative pseudo-equality algebras

Pseudo-equality algebras were initially introduced by Jenei and Kóródi as a possible algebraic semantic for fuzzy-type theory, and they have been revised by Dvureăźenskij and Zahiri under the name of JK-algebras. In this paper, we define and study the ...
Building small equality graphs for deciding equality logic with uninterpreted functions

The logic of Equalities with Uninterpreted Functions is used in the formal verification community mainly for proofs of equivalence: proving that two versions of a hardware design are the same, or that input and output of a compiler are semantically ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

CAV '98: Proceedings of the 10th International Conference on Computer Aided Verification

June 1998

550 pages

ISBN:3540646086

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 28 June 1998

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

22
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Velev MGao P(2011)Automatic formal verification of reconfigurable DSPsProceedings of the 16th Asia and South Pacific Design Automation Conference10.5555/1950815.1950881(293-296)Online publication date: 25-Jan-2011
https://dl.acm.org/doi/10.5555/1950815.1950881
Velev MGao P(2010)Method for formal verification of soft-error tolerance mechanisms in pipelined microprocessorsProceedings of the 12th international conference on Formal engineering methods and software engineering10.5555/1939864.1939894(355-370)Online publication date: 17-Nov-2010
https://dl.acm.org/doi/10.5555/1939864.1939894
Velev MGao PLin Y(2010)A method for debugging of pipelined processors in formal verification by correspondence checkingProceedings of the 2010 Asia and South Pacific Design Automation Conference10.5555/1899721.1899866(619-624)Online publication date: 18-Jan-2010
https://dl.acm.org/doi/10.5555/1899721.1899866
Mokhtari YAbed SAit Mohamed OTahar SSong X(2008)A New Approach for the Construction of Multiway Decision GraphsProceedings of the 5th international colloquium on Theoretical Aspects of Computing10.1007/978-3-540-85762-4_16(228-242)Online publication date: 1-Sep-2008
https://dl.acm.org/doi/10.1007/978-3-540-85762-4_16
Rodeh YStrichman O(2006)Building small equality graphs for deciding equality logic with uninterpreted functionsInformation and Computation10.5555/1140956.1709620204:1(26-59)Online publication date: 1-Jan-2006
https://dl.acm.org/doi/10.5555/1140956.1709620
Velev M(2006)Using Abstraction for Efficient Formal Verification of Pipelined Processors with Value PredictionProceedings of the 7th International Symposium on Quality Electronic Design10.1109/ISQED.2006.142(51-56)Online publication date: 27-Mar-2006
https://dl.acm.org/doi/10.1109/ISQED.2006.142
Velev M(2005)Automatic formal verification of liveness for pipelined processors with multicycle functional unitsProceedings of the 13 IFIP WG 10.5 international conference on Correct Hardware Design and Verification Methods10.1007/11560548_10(97-113)Online publication date: 3-Oct-2005
https://dl.acm.org/doi/10.1007/11560548_10
van de Pol JTveretina O(2005)A BDD-Representation for the logic of equality and uninterpreted functionsProceedings of the 30th international conference on Mathematical Foundations of Computer Science10.1007/11549345_66(769-780)Online publication date: 29-Aug-2005
https://dl.acm.org/doi/10.1007/11549345_66
Meir OStrichman O(2005)Yet another decision procedure for equality logicProceedings of the 17th international conference on Computer Aided Verification10.1007/11513988_32(307-320)Online publication date: 6-Jul-2005
https://dl.acm.org/doi/10.1007/11513988_32
Velev M(2004)Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of MicroprocessorsProceedings of the conference on Design, automation and test in Europe - Volume 110.5555/968878.969033Online publication date: 16-Feb-2004
https://dl.acm.org/doi/10.5555/968878.969033
Show More Cited By

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

Cited By

Recommendations

BDD Based Procedures for a Theory of Equality with Uninterpreted Functions

Commutative pseudo-equality algebras

Building small equality graphs for deciding equality logic with uninterpreted functions

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations