Skip to main content
SpringerLink
Log in

Introductory Paper

  • Special section on Recent Advances in Hardware Verification
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

In today’s competitive market designing of digital systems (hardware as well as software) faces tremendous challenges. In fact, notwithstanding an ever decreasing project budget, time to market and product lifetime, designers are faced with an ever increasing system complexity and customer expected quality. The above situation calls for better and better formal verification techniques at all steps of the design flow. This special issue is devoted to publishing revised versions of contributions first presented at the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME) held 21–24 October 2003 in L’Aquila, Italy. Authors of well regarded papers from CHARME’03 were invited to submit to this special issue. All papers included here have been suitably extended and have undergone an independent round of reviewing.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. National Institute of Standards and Technology: The economic impacts of inadequate infrastructure for software testing. Planning Report 02–3. National Institute of Standards and Technology (2002)

  2. Fitzpatrick, T., Schutten, R.: Design for verification: Blueprint for productivity and product quality. Technical report, Synopsy Inc., 2003. http://www.synopsys.com/products/simulation/dfv_wp.html

  3. Collett International Research Inc. IC/ASIC functional verification study. Technical report, Collett International Research Inc. (2002) http://www.collett.com/reports.htm

  4. Geist, D., Tronci, E. (eds.): Correct Hardware Design and Verification Methods (CHARME), vol. 2860 of Lecture Notes in Computer Science, L’Aquila, Italy. 12th IFIP WG 10.5 Advanced Research Working Conference. Springer, Berlin (2003)

  5. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge, MA (1999)

    Google Scholar 

  6. Clarke, E.M., Emerson, E.A.: Synthesis of synchronization skeletons for branching time temporal logic. In: Logic of Programs: Workshop, vol. 131 of Lecture Notes in Computer Science, Springer-Verlag, Yorktown Heights, NY (1981)

  7. Emerson, E.A., Clarke, E.M., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Languages Syst. 8(2), 244–263 (1986)

    Article  Google Scholar 

  8. Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer and Processors, pp. 522–525. IEEE Computer Society, Washington, DC (1992)

  9. Holzmann, G.J.: The SPIN Model Checker, Primer and Reference manual. Addison-Wesley, Reading, MA (2003)

    Google Scholar 

  10. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput. 98(2), 142–170 (1992)

    Article  MathSciNet  Google Scholar 

  11. McMillan, K.L.: Symbolic Model Checking. Kluwer, Dordretch (1993)

    MATH  Google Scholar 

  12. Bryant, R.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput C-35(8), 677–691 (1986)

    Google Scholar 

  13. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bdds. In: Cleaveland, W.R. (ed.) Proceedings of 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS’99, vol. 1579 of LNCS. Springer, Amsterdam, The Netherlands (1999)

  14. Zhang, L., Malik, S.: The quest for efficient boolean satisfiability solvers. In: Proceedings of 14th Conference on Computer Aided Verification (CAV), Lecture Notes in Computer Science. Springer-Verlag, Copenhagen, Denmark (2002)

  15. Hu, A.J., York, G., Dill, D.L.: New techniques for efficient verification with implicitly conjoined BDDs. In: 31st ACM/IEEE Design Automation Conference (DAC). San Diego Convention Center, San Diego, CA (1994)

  16. Della Penna, G., Intrigila, B., Melatti, I., Minichino, M., Ciancamerla, E., Parisse, A., Tronci, E., Zilli, M.V.: Automatic verification of a turbogas control system with the murφ verifier. In: Maler, O., Pnueli, A. (eds.) Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3–5, 2003, Proceedings, vol. 2623 of Lecture Notes in Computer Science, pp. 141–155. Springer, Berlin (2003)

  17. Spin web page: http://spinroot.com

  18. Murphi web page: http://sprout.stanford.edu/dill/murphi.html

  19. Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, R.C., Laubach, S., Zheng, H.: Bandera: Extracting finite-state models from java source code. In: Proceedings of the 22nd International Conference on Software Engineering (2000)

  20. Bandera web page: http://bandera.projects.cis.ksu.edu/index.shtml.

  21. Havelund, K., Pressburger, T.: Model checking java programs using java pathfinder. Int. J. Software Tools Technol. Transfer 2 (4), April (2000)

  22. Java pathfinder web page: http://ase.arc.nasa.gov/havelund/jpf.html

  23. Holzmann, G., Smith, M.: A practical method for verifying event driven software. In: Proceedings of ACM/IEEE International Conference on Software Engineering (ICSE). ACM/IEEE, New York (1999)

  24. Feaver web page: http://cm.bell-labs.com/cm/cs/what/feaver/

  25. Della Penna, G., Intrigila, B., Melatti, I., tronci, E., Zilli, M.: Exploiting transition locality in automatic verification of concurrent systems. International Journal on Software Tools for Technology Transfer 6 (4) (2004)

  26. Caching murphi web page: http://www.dsi.uniroma1.it/~tronci/cached.murphi.html

  27. Smv web page: http://www.cs.cmu.edu/~modelcheck/

  28. Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In: Proceedings of International Conference on Computer-Aided Verification (CAV 2002), vol. 2404 of LNCS. Springer, Copenhagen, Denmark (2002)

  29. Nusmv web page: http://nusmv.irst.itc.it

  30. Brayton, R.K., Hachtel, G.D., Sangiovanni-Vincentelli, A., Somenzi, F., Aziz, A., Cheng, S.-T., Edwards, S., Khatri, S., Kukimoto, Y., Pardo, A., Qadeer, S., Ranjan, R.K., Sarwary, S., Shiple, T.R., Swamy, G., Villa, T.: Vis: A system for verification and synthesis. In: Proceedings of Computer Aided Verification (CAV), Lecture Notes in Computer Science. Springer, Berlin (1996)

  31. Vis web page: http://vlsi.colorado.edu/vis

  32. Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL: Status and developments. In: Grumberg, O. (ed.) Proc. of Computer 9th Intern. Conf. on Computer Aided Verification (CAV), vol. 1254 of Lecture Notes in Computer Science, pp. 456–459. Springer, Haifa, Israel (1997)0

  33. Uppaal web page: http://www.uppaal.com/

  34. Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) Proceedings of the 8th International SPIN Workshop on Model Checking Software, vol. 2057 of LNCS, pp 103–122, Springer, Toronto, Canada (2001)

  35. Slam web page: http://research.microsoft.com/projects/slam/

  36. Baier, C., Clarke, E.M., Hartonas-Garmhausen, V., Kwiatkowska, M., Ryan, M.: Symbolic model checking for probabilistic processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) Automata, Languages and Programming, 24th International Colloquium, ICALP’97, Bologna, Italy, Proceedings, vol. 1256 of Lecture Notes in Computer Science, pp. 430–440. Springer, Berlin (1997)

  37. Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: A hybrid approach. In: Katoen, J.P., Stevens, P. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, Proceedings, vol. 2280 of Lecture Notes in Computer Science, pp. 52–66. Springer, Berlin (2002)

  38. Prism web page: http://www.cs.bham.ac.uk/~dxp/prism/

  39. Moore, J.S.: Inductive assertions and operational semantics. Int. J. Software Tools Technol. Transfer XX, XX (XXXX)

  40. Beyer, S., Jacobi, C., Kröning, D., Leinenbach1, D., Paul, W.J.: Putting it all together–-formal verification of the vamp. Int. J. Software Tools Technol. Transfer XX, XX (XXXX)

  41. Chockler, H., Kupfermann, O., Vardi, M.Y.: Coverage metrics for formal verification. Int. J. Software Tools Technol. Transfer XX, XX (XXXX)

  42. Ganay, M.K., Gupta, A., Yang, Z., Ashar, P.: Efficient distributed sat and sat based distributed bounded model checking. Int. J. Software Tools Technol. Transfer XX, XX (XXXX)

  43. Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V.: Finite horizon analysis of markov chains with the murφ verifier. Int. J. Software Tools Technol. Transfer XX, XX (XXXX)

  44. Fisler, K.: Towards diagrammability and efficiency in event sequence languages. Int. J. Software Tools Technol. Transfer XX, XX (XXXX)

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università di Roma “La Sapienza”, Via Salaria 113, 00198, Rome, Italy

    Enrico Tronci

Authors
  1. Enrico Tronci
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Enrico Tronci.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Tronci, E. Introductory Paper. Int J Softw Tools Technol Transfer 8, 355–358 (2006). https://doi.org/10.1007/s10009-005-0212-y

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-005-0212-y

Keywords

Search

Navigation