nach oben

Erschienen in:

2011 | OriginalPaper | Buchkapitel

3. Related Work

verfasst von : Sudipta Kundu, Sorin Lerner, Rajesh K. Gupta

Erschienen in: High-Level Verification

Verlag: Springer New York

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Each one of the three areas of high-level verificationoutlined in Chap. 1, namely high-level property checking, translation validation, and synthesis tool verification, have been explored in a wide variety of research efforts. In this chapter, we discuss various techniques from each of these areas that are directly relevant to this book.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Background

Nächstes Kapitel Verification Using Automated Theorem Provers

Ashar, P., Bhattacharya, S., Raghunathan, A., Mukaiyama, A.: Verification of RTL generated from scheduled behavior in a high-level synthesis flow. In: ICCAD ’98: Proceedings of the 1998 IEEE/ACM International Conference on Computer-Aided Design, pp. 517–524 (1998). URL citeseer.ist.psu.edu/ashar98verification.html

Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., Ustuner, A.: Thorough static analysis of device drivers. In: EuroSys ’06: Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems 2006, pp. 73–85. ACM, New York, NY, USA (2006). DOI http://doi.acm.org/10.1145/1217935.1217943

Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. In: PLDI ’01: Proceedings of the 2001 ACM SIGPLAN conference on Programming Language Design and Implementation (2001). URL citeseer.ist.psu.edu/ball01automatic.html

14.

Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker blast: Applications to software engineering. International Journal on Software Tools for Technology Transfer 9(5), 505–525 (2007). DOI http://dx.doi.org/10.1007/s10009-007-0044-z

15.

Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using sat procedures instead of bdds. In: DAC ’99: Proceedings of the 36th ACM/IEEE conference on Design automation, pp. 317–320. ACM, New York, NY, USA (1999). DOI http://doi.acm.org/10.1145/309847.309942

17.

Blank, C.: Formal verification of register binding. In: WAVE ’00: Proceedings of the Workshop on Advances in Verification (2000)

18.

Borrione, D., Dushina, J., Pierre, L.: A compositional model for the functional verification of high-level synthesis results. IEEE Transactions on Very Large Scale Integration (VLSI) Systems 8(5), 526–530 (2000). DOI http://dx.doi.org/10.1109/92.894157

22.

Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24(3), 293–318 (1992)CrossRef

23.

Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic Model Checking: 10²⁰ States and Beyond. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 1–33. IEEE Computer Society Press, Washington, D.C. (1990). URL citeseer.ist.psu.edu/burch90symbolic.html

28.

Chaki, S., Clarke, E., Groce, A.: Modular verification of software components in C. In: IEEE Transactions on Software Engineering, pp. 385–395 (2003)

31.

Clarke, E., Kroening, D., Yorav, K.: Behavioral consistency of c and verilog programs using bounded model checking. In: DAC ’03: Proceedings of the 40th Conference on Design automation, pp. 368–371. ACM, New York, NY, USA (2003). DOI http://doi.acm.org/10.1145/775832.775928

34.

Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional model checking. Tech. Rep. CMS-CS-89-145, School of Computer Science, Canergie Mellon University (1989)

35.

C.N. Ip, D.L. Dill: Better verification through symmetry. In: D. Agnew, L. Claesen, R. Camposano (eds.) Computer Hardware Description Languages and their Applications, pp. 87–100. Elsevier Science Publishers B.V., Amsterdam, Netherland, Ottawa, Canada (1993). URL citeseer.ist.psu.edu/ip96better.html

38.

Corporation, I.: Rational Statemate. www.telelogic.com/products/statemate

39.

Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM Symposium on Principles of Programming Languages, pp. 238–252. Los Angeles CA (1977)

41.

Cousot, P., Cousot, R.: Systematic design of program transformation frameworks by abstract interpretation. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Portland OR (2002)

42.

Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 84–97. ACM Press, New York, NY, Tucson, Arizona (1978)

43.

Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: CAV ’99: Proceedings of the 11th International Conference on Computer Aided Verification, pp. 160–171. Springer-Verlag, London, UK (1999)

46.

Dill, D.L.: The murphi verification system. In: CAV ’96: Proceedings of the 8th International Conference on Computer Aided Verification, pp. 390–393. Springer-Verlag, London, UK (1996)

47.

Dushina, J., Borrione, D., Jerraya, A.A.: Formal verification of the allocation step in high level synthesis. In: Forum on Design Languages (FDL’98). Lausanne, Switzerland (1998). URL citeseer.ist.psu.edu/57380.html

51.

Eisenbiegler, D., Blumenröhr, C., Kumar, R.: Implementation issues about the embedding of existing high level synthesis algorithms in hol. In: TPHOLs ’96: Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, pp. 157–172. Springer-Verlag, London, UK (1996)

53.

Emerson, F.A., Sistla, A.P.: Symmetry and model checking. Formal Methods in System Design: An International Journal 9(1/2), 105–131 (1996). URL citeseer.ist.psu.edu/emerson94symmetry.html

54.

Eveking, H., Hinrichsen, H., Ritter, G.: Automatic verification of scheduling results in high-level synthesis. In: DATE ’99: Proceedings of the conference on Design, automation and test in Europe, p. 12. ACM Press, New York, NY, USA (1999). DOI http://doi.acm.org/10.1145/307418.307449

57.

Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of the 32nd ACM Symposium on Principles of Programming Languages (2005)

70.

Godefroid, P.: Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem. Ph.D. thesis, Univerite De Liege (1995). URL citeseer.ist.psu.edu/godefroid95partialorder.html

71.

Godefroid, P.: Model checking for programming languages using VeriSoft. In: Proceedings of the 24th ACM Symposium on Principles of Programming Languages (1997)

75.

Gordon, M.: HOL: A proof generating system for higher-order logic. In: G. Birtwistle, P. Subrahmanyam (eds.) VLSI Specification Verification and Synthesis, pp. 73–128. Kluwer Academic Publishers (1988)

76.

Graf, S., Saidi, H.: Construction of abstract state graphs of infinite systems with PVS. In: CAV ’97: Proceedings of the international conference on Computer Aided Verification (1997)

83.

Gupta, R.K., Liao, S.Y.: Using a programming language for digital system design. IEEE Design and Test 14(2), 72–80 (1997). DOI http://dx.doi.org/10.1109/54.587745

87.

Hanna, F.K., Daeche, N., Longley, M.: Formal Synthesis of Digital Systems. In: L. Claesen (ed.) Proc IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, pp. 532–548. Elsevier (1989). URL http://www.cs.kent.ac.uk/pubs/1989/422. Leuven, Belgium

89.

Helmstetter, C., Maraninchi, F., Maillet-Contoz, L., Moy, M.: Automatic generation of schedulings for improving the test coverage of Systems-on-a-Chip. In: FMCAD ’06: Proceedings of the Formal Methods in Computer Aided Design, pp. 171–178. IEEE Computer Society, Washington, DC, USA (2006). DOI http://dx.doi.org/10.1109/FMCAD.2006.10

90.

Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th ACM Symposium on Principles of Programming Languages (2002)

91.

Hinrichsen, H.: Language of labelled segments documentation. Tech. rep., Darmstadt University of Technology (1998). URL http://www.rs.e-technik.tudarmstadt.de/∼hinni/document/index.html

94.

Holzmann, G.J.: The model checker SPIN. Software Engineering 23(5), 279–295 (1997). URL citeseer.ist.psu.edu/holzmann97model.html

97.

Ivanicic, F., Yang, Z., Ganai, M.K., Gupta, A., Ashar, P.: Efficient sat-based bounded model checking for software verification. Theoretical Computer Science 404(3), 256–274 (2008). DOI http://dx.doi.org/10.1016/j.tcs.2008.03.013

98.

Johnson, S., Bose, B.: DDD — a system for mechanized digital design derivation. In: ACM/SIGDA Workshop on Formal Methods in VLSI Design. Miami, Florida (1991). URL citeseer.ist.psu.edu/johnson97ddd.html

106.

Karfa, C., Mandal, C., Sarkar, D., Pentakota, S.R., Reade, C.: A formal verification method of scheduling in high-level synthesis. IEEE International Symposium on Quality Electronic Design 0, 71–78 (2006). DOI http://doi.ieeecomputersociety.org/10.1109/ISQED.2006.10

111.

Kim, Y., Kopuri, S., Mansouri, N.: Automated formal verification of scheduling process using finite state machines with datapath (fsmd). In: ISQED ’04: Proceedings of the 5th International Symposium on Quality Electronic Design, pp. 110–115. IEEE Computer Society, Washington, DC, USA (2004)

112.

Koelbl, A., Burch, J.R., Pixley, C.: Memory modeling in ESL-RTL equivalence checking. In: DAC ’07: Proceedings of the 44th annual conference on Design automation, pp. 205–209. ACM, New York, NY, USA (2007). DOI http://doi.acm.org/10.1145/1278480.1278530

122.

Lahiri, S.K., Ball, T., Cook, B.: Predicate abstraction via symbolic decision procedures. In: CAV ’05: Proceedings of the 17th International Conference on Computer Aided Verification, pp. 24–38 (2005)

126.

Larsson, M.: Improving the result of high-level synthesis using interactive transformational design. In: TPHOLs ’96: Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, pp. 299–314. Springer-Verlag, London, UK (1996)

138.

Mansouri, N., Vemuri, R.: Automated correctness condition generation for formal verification of synthesized RTL designs. Formal Methods in System Design: An International Journal 16(1), 59–91 (2000). URL citeseer.ist.psu.edu/mansouri99automated.html

141.

McFarland, M.C.: Formal analysis of correctness of behavioral transformations. Formal Methods in System Design 2(3), 231–257 (1993). DOI http://dx.doi.org/10.1007/BF01384133

144.

McMillan, K.L.: A methodology for hardware verification using compositional model checking. Science of Computer Programming 37(1-3), 279–309 (2000)MATHCrossRef

146.

Mendías, J.M., Hermida, R., Molina, M.C., Penalba, O.: Efficient verification of scheduling, allocation and binding in high-level synthesis. In: DSD ’02: Proceedings of the Euromicro Symposium on Digital Systems Design, p. 308. IEEE Computer Society, Washington, DC, USA (2002)

150.

Moore, J.S.: Symbolic simulation: An acl2 approach. In: Proceedings of Formal Methods in Computer-Aided Design, pp. 334–350 (1998). URL citeseer.ist.psu.edu/moore98symbolic.html

151.

Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of the 38th Design Automation Conference (DAC’01) (2001). URL citeseer.ist.psu.edu/moskewicz01chaff.html

152.

Moura, L.D., Bjrner, N.: Z3: An efficient smt solver. In: TACAS ’08: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2008)

155.

Musuvathi, M., Park, D.Y.W., Chou, A., Engler, D.R., Dill, D.L.: CMC: A pragmatic approach to model checking real code. In: Proceedings of the Fifth Symposium on Operating Systems Design and Implementation (2002)

156.

Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: PLDI ’07: Proceedings of the 2007 ACM SIGPLAN conference on Programming Language Design and Implementation, pp. 446–455. ACM, New York, NY, USA (2007)

157.

Narasimhan, N.: Theorem proving guided development of formal assertions and their embedding in a high-level vlsi synthesis system. Ph.D. thesis, University of Cincinnati (1998)

158.

Narasimhan, N., Teica, E., Radhakrishnan, R., Govindarajan, S., Vemuri, R.: Theorem proving guided development of formal assertions in a resource-constrained scheduler for high-level synthesis. Formal Methods in System Design 19(3), 237–273 (2001). DOI http://dx.doi.org/10.1023/A:1011250531814

159.

Narasimhan, N., Vemuri, R.: On the effectiveness of theorem proving guided discovery of formal assertions for a register allocator in a high-level synthesis system. In: J. Grundy, M. Newey (eds.) Theorem Proving in Higher Order Logics: 11th International Conference, TPHOLs ’98, pp. 367–386. Springer-Verlag, Canberra, Australia (1998). URL citeseer.ist.psu.edu/341177.html

164.

Owre, S., Rushby, J.M.,, Shankar, N.: PVS: A prototype verification system. In: D. Kapur (ed.) Proceedings of 11th International Conference on Automated Deduction (CADE), Lecture Notes in Artificial Intelligence, vol. 607, pp. 748–752. Springer-Verlag, Saratoga, NY (1992). DOI http://www.csl.sri.com/papers/cade92-pvs/

165.

Paulson, L.C.: Isabelle: A generic theorem prover, Lecure Notes in Computer Science, vol. 828. Springer Verlag (1994)

175.

Radhakrishnan, R., Teica, E., Vermuri, R.: An approach to high-level synthesis system validation using formally verified transformations. In: HLDVT ’00: Proceedings of the IEEE International High-Level Validation and Test Workshop (HLDVT’00), p. 80. IEEE Computer Society, Washington, DC, USA (2000)

176.

Rajan, S.P.: Correctness of transformations in high level synthesis. In: S.D. Johnson (ed.) CHDL ’95: 12th Conference on Computer Hardware Description Languages and their Applications, pp. 597–603. Chiba, Japan (1995). URL citeseer.ist.psu.edu/rajan95correctness.html

185.

Sharp, R., Rasmussen, O.: The T-Ruby design system. Formal Methods in System Design: An International Journal 11(3), 239–264 (1997). URL citeseer.ist.psu.edu/article/sharp95truby.html

193.

Systems, C.D.: Slec system. www.calypto.com/slecsystem.php

194.

Technologies, E.: Scade design verifier. www.esterel-technologies.com/

196.

The VIS Group, R.K.B., Sangiovanni-Vincentelli, A.L.: Vis: A system for verification and synthesis. Tech. Rep. UCB/ERL M95/104, EECS Department, University of California, Berkeley (1995). URL http://www.eecs.berkeley.edu/Pubs/TechRpts/1995/2923.html

202.

Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. In: Automated Software Engineering Journal, pp. 3–12. Press (2000)

212.

Zuck, L., Pnueli, A., Fang, Y., Goldberg, B.: VOC: A methodology for the translation validation of optimizing compilers. Journal of Universal Computer Science 9(3), 223–247 (2003)

Titel: Related Work
verfasst von: Sudipta Kundu
Sorin Lerner
Rajesh K. Gupta
Verlag: Springer New York
Buch: High-Level Verification
Print ISBN: 978-1-4419-9358-8

Electronic ISBN: 978-1-4419-9359-5

Copyright-Jahr: 2011
DOI: https://doi.org/10.1007/978-1-4419-9359-5_3

Neuer Inhalt

Bildnachweise

VDI-Icon, Profil Icon, inhalt2, Springer Professional Modul/© Springer Fachmedien Wiesbaden GmbH, Nachhaltigkeitsaward Key Visual/© Cometis AG/Global ESG Monitor | Daniel Rupp | Generiert mit KI, Search Icon, Banner Hanser, Beijing Auto Show 2024: Deutsche Hersteller wollen angreifen./© EKH-Pictures / Generated with AI / Stock.adobe.com, Buchstaben, die aus einem Megaphon kommen/© MicroStockHub/Getty Images/iStock, Digitale Lieferkette/© zapp2photo / stock.adobe.com, Zeitschrift Wissensmanagement Cover, PatentFit-Logo/© Springer Fachmedien Wiesbaden GmbH, Sustainibility Finance/© Robert Kneschke / stock.adobe.com / Springer Fachmedien Wiesbaden GmbH, Zukunftswerkstatt Sales Excellence 2024/© AndreyPopov / Getty Images / iStock, 2023_Antrieb/© supervisuell

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Neuer Inhalt

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.