Top

Published in:

2011 | OriginalPaper | Chapter

3. Related Work

Authors : Sudipta Kundu, Sorin Lerner, Rajesh K. Gupta

Published in: High-Level Verification

Publisher: Springer New York

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

previous chapter Background

next chapter 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)

Title: Related Work
Authors: Sudipta Kundu
Sorin Lerner
Rajesh K. Gupta
Publisher: Springer New York
Book: High-Level Verification
Print ISBN: 978-1-4419-9358-8

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

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

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"