nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools

verfasst von : Reiner Hähnle, Marieke Huisman

Erschienen in: Computing and Software Science

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

Deductive software verification aims at formally verifying that all possible behaviors of a given program satisfy formally defined, possibly complex properties, where the verification process is based on logical inference. We follow the trajectory of the field from its inception in the late 1960s via its current state to its promises for the future, from pen-and-paper proofs for programs written in small, idealized languages to highly automated proofs of complex library or system code written in mainstream languages. We take stock of the state-of-art and give a list of the most important challenges for the further development of the field of deductive software verification.

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 Language-Driven Engineering: From General-Purpose to Purpose-Specific Languages

Nächstes Kapitel Static Analysis for Proactive Security

We use Java terminology for what is also called procedure, function, subroutine, etc.

The first verification system based on dynamic logic is reported in [95], but it was based on an axiomatic calculus and had no further impact.

http://www.verifythis.org/.

However, Eiffel contracts were intended for runtime (rather than static) verification.

There is a whole conference series devoted to this topic, see https://en.wikipedia.org/wiki/International_Conference_on_Software_Reuse.

Relating to formal methods-based software tools in general, the journal Software Tools for Technology Transfer (STTT), as well as the conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS), were established as dedicated venues to foster tool integration and maturation. The article [118] discusses the history and the challenges of this endeavor, see also I.7.

http://www.cs.utexas.edu/~moore/acl2/.

https://github.com/boogie-org/boogie.

http://www.key-project.org/.

http://www.isse.uni-augsburg.de/en/software/kiv/.

http://www.openjml.org/.

http://www.adacore.com/sparkpro/.

http://krakatoa.lri.fr/.

https://deepspec.org/.

Abrial, J.-R.: The B Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)CrossRef

Ackerman, E.: Hail, robo-taxi!. IEEE Spectr. 54(1), 26–29 (2017)CrossRef

Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P., Ulbrich, M. (eds.): Deductive Software Verification-The KeY Book: From Theory to Practice. LNCS, vol. 10001. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-319-49812-6CrossRef

Alglave, J., Donaldson, A.F., Kroening, D., Tautschnig, M.: Making software verification tools really work. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 28–42. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24372-1_3CrossRef

Ameri, M., Furia, C.A.: Why just boogie? Translating between intermediate verification languages. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 79–95. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33693-0_6CrossRef

Amighi, A., Blom, S., Darabi, S., Huisman, M., Mostowski, W., Zaharieva-Stojanovski, M.: Verification of concurrent systems with VerCors. In: Bernardo, M., Damiani, F., Hähnle, R., Johnsen, E.B., Schaefer, I. (eds.) SFM 2014. LNCS, vol. 8483, pp. 172–216. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-07317-0_5CrossRef

Amighi, A., Blom, S., Huisman, M.: Resource protection using atomics. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 255–274. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-12736-1_14CrossRef

Amighi, A., Blom, S., Huisman, M.: VerCors: a layered approach to practical verification of concurrent software. In: 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP, Heraklion, Crete, Greece, pp. 495–503. IEEE Computer Society (2016)

Amighi, A., Haack, C., Huisman, M., Hurlin, C.: Permission-based separation logic for multithreaded Java programs. Logical Methods Comput. Sci. 11(1) (2015)

10.

Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006). https://doi.org/10.1007/11804192_17CrossRef

11.

Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30569-9_3CrossRef

12.

Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, UK (2010)

13.

Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Lessons learned from microkernel verification - specification is the new bottleneck. In: Cassez, F., Huuck, R., Klein, G., Schlich, B. (eds.) Proceedings of the 7th Conference on Systems Software Verification. EPTCS, vol. 102, pp. 18–32 (2012)CrossRef

14.

Beckert, B., Grebing, S., Böhl, F.: A usability evaluation of interactive theorem provers using focus groups. In: Canal, C., Idani, A. (eds.) SEFM 2014. LNCS, vol. 8938, pp. 3–19. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-15201-1_1CrossRef

15.

Beckert, B., Klebanov, V., Ulbrich, M.: Regression verification for Java using a secure information flow calculus. In: Monahan, R. (ed.) Proceedings of the 17th Workshop on Formal Techniques for Java-Like Programs, FTfJP, Prague, Czech Republic, pp. 6:1–6:6. ACM (2015)

16.

Beckert, B., Schlager, S.: Software verification with integrated data type refinement for integer arithmetic. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 207–226. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24756-2_12CrossRefMATH

17.

Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: exchanging verification results between verifiers. In: Zimmermann, T., Cleland-Huang, J., Su, Z. (eds.) Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE, Seattle, WA, USA, pp. 326–337. ACM (2016)

18.

Beyer, D., Lemberger, T.: Symbolic execution with CEGAR. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 195–211. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_14CrossRef

19.

Bjørner, N., Browne, A., Colón, M., Finkbeiner, B., Manna, Z., Sipma, H., Uribe, T.E.: Verifying temporal properties of reactive systems: a step tutorial. Formal Methods Syst. Des. 16(3), 227–270 (2000)CrossRef

20.

Blom, S., Huisman, M.: The VerCors tool for verification of concurrent programs. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 127–131. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06410-9_9CrossRef

21.

Blom, S., Huisman, M., Kiniry, J.: How do developers use APIs? A case study in concurrency. In: International Conference on Engineering of Complex Computer Systems (ICECCS), Singapore, pp. 212–221. IEEE Computer Society (2013)

22.

Blom, S., Huisman, M., Mihelčić, M.: Specification and verification of GPGPU programs. Sci. Comput. Program. 95, 376–388 (2014)CrossRef

23.

Blom, S., Huisman, M., Zaharieva-Stojanovski, M.: History-based verification of functional behaviour of concurrent programs. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 84–98. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22969-0_6CrossRef

24.

Bobot, F., Filliâtre, J.-C., Marché, C., Paskevich, A.: Why3: shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages (2011)

25.

Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, Long Beach, California, USA, pp. 259–270. ACM (2005)

26.

Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-44898-5_4CrossRef

27.

Brain, M., Tinelli, C., Rümmer, P., Wahl, T.: An automatable formal semantics for IEEE-754 floating-point arithmetic. In: 22nd IEEE Symposium on Computer Arithmetic, ARITH 2015, Lyon, France, pp. 160–167. IEEE (2015)

28.

Brookes, S.: A semantics for concurrent separation logic. Theoret. Comput. Sci. 375(1–3), 227–270 (2007)MathSciNetCrossRef

29.

Brookes, S., O’Hearn, P.: Concurrent separation logic. ACM SIGLOG News 3(3), 47–65 (2016)

30.

Bubel, R., Damiani, F., Hähnle, R., Johnsen, E.B., Owe, O., Schaefer, I., Yu, I.C.: Proof repositories for compositional verification of evolving software systems. In: Steffen, B. (ed.) Transactions on Foundations for Mastering Change I. LNCS, vol. 9960, pp. 130–156. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46508-1_8CrossRef

31.

Burstall, R.M.: Program proving as hand simulation with a little induction. In: Information Processing 1974, pp. 308–312. Elsevier/North-Holland, Amsterdam (1974)

32.

Calcagno, C., Distefano, D.: Infer: an automatic program verifier for memory safety of C programs. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 459–465. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_33CrossRef

33.

Cheon, Y., Leavens, G., Sitaraman, M., Edwards, S.: Model variables: cleanly supporting abstraction in design by contract. Softw. Pract. Exp. 35, 583–599 (2005)CrossRef

34.

Chimento, J.M., Ahrendt, W., Pace, G.J., Schneider, G.: StaRVOOrS: a tool for combined static and runtime verification of Java. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 297–305. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23820-3_21CrossRefMATH

35.

Christakis, M., Müller, P., Wüstholz, V.: An experimental evaluation of deliberate unsoundness in a static program analyzer. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 336–354. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46081-8_19CrossRef

36.

Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_2CrossRef

37.

Cok, D.: OpenJML: software verification for Java 7 using JML, OpenJDK, and Eclipse. In: Dubois, C., Giannakopoulou, D., Méry, D. (eds.) 1st Workshop on Formal Integrated Development Environment, (F-IDE). EPTCS, vol. 149, pp. 79–92 (2014)CrossRef

38.

Cok, D.R., Kiniry, J.R.: ESC/Java2: uniting ESC/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108–128. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30569-9_6CrossRef

39.

de Gouw, S., Rot, J., de Boer, F.S., Bubel, R., Hähnle, R.: OpenJDK’s Java.utils.Collection.sort() is broken: the good, the bad and the worst case. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 273–289. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_16CrossRef

40.

de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24CrossRef

41.

Deussen, P., Hansmann, A., Käufl, T., Klingenbeck, S.: The verification system Tatzelwurm. In: Broy, M., Jähnichen, S. (eds.) KORSO: Methods, Languages, and Tools for the Construction of Correct Software. LNCS, vol. 1009, pp. 285–298. Springer, Heidelberg (1995). https://doi.org/10.1007/BFb0015468CrossRef

42.

Dijkstra, E.: A Discipline of Programming. Prentice-Hall, Upper Saddle River (1976)MATH

43.

Din, C.C., Bubel, R., Hähnle, R.: KeY-ABS: a deductive verification tool for the concurrent modelling language ABS. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 517–526. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_35CrossRef

44.

Do, Q.H., Bubel, R., Hähnle, R.: Exploit generation for information flow leaks in object-oriented programs. In: Federrath, H., Gollmann, D. (eds.) SEC 2015. IAICT, vol. 455, pp. 401–415. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-18467-8_27CrossRef

45.

Ernst, G., Pfähler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV: overview and verifythis competition. STTT 17(6), 677–694 (2015)CrossRef

46.

Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1–3), 35–45 (2007)MathSciNetCrossRef

47.

Filliâtre, J.-C., Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73368-3_21CrossRef

48.

Floyd, R.W.: Assigning meanings to programs. Proc. Symp. Appl. Math 19, 19–31 (1967)MathSciNetCrossRef

49.

Fulton, N., Mitsch, S., Quesel, J.-D., Völp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 527–538. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_36CrossRef

50.

Giesl, J., et al.: Proving termination of programs automatically with AProVE. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 184–191. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08587-6_13CrossRef

51.

Hähnle, R., Heisel, M., Reif, W., Stephan, W.: An interactive verification system based on dynamic logic. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 306–315. Springer, Heidelberg (1986). https://doi.org/10.1007/3-540-16780-3_99CrossRef

52.

Kamburjan, E., Hähnle, R.: Uniform modeling of railway operations. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2016. CCIS, vol. 694, pp. 55–71. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-53946-1_4CrossRef

53.

Hähnle, R., Menzel, W., Schmitt, P.: Integrierter deduktiver Software-Entwurf. Künstliche Intelligenz, pp. 40–41, December 1998

54.

Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. Foundations of Computing. MIT Press, Cambridge (2000)CrossRef

55.

Heisel, M., Reif, W., Stephan, W.: Program verification by symbolic execution and induction. In: Morik, K. (ed.) GWAI-87 11th German Workshop on Artifical Intelligence. Informatik-Fachberichte, vol. 152, pp. 201–210. Springer, Heidelberg (1987). https://doi.org/10.1007/978-3-642-73005-4_22CrossRef

56.

Hentschel, M., Bubel, R., Hähnle, R.: Symbolic execution debugger (SED). In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 255–262. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11164-3_21CrossRef

57.

Hentschel, M., Hähnle, R., Bubel, R.: An empirical evaluation of two user interfaces of an interactive program verifier. In: Lo, D., Apel, S., Khurshid, S. (eds.) Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering (ASE), Singapore, pp. 403–413. ACM Press, September 2016

58.

Hentschel, M., Hähnle, R., Bubel, R.: The interactive verification debugger: effective understanding of interactive proof attempts. In: Lo, D., Apel, S., Khurshid, S. (eds.) Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering (ASE), Singapore, pp. 846–851. ACM Press, September 2016

59.

Hentschel, M., Käsdorf, S., Hähnle, R., Bubel, R.: An interactive verification tool meets an IDE. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 55–70. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10181-1_4CrossRef

60.

Hoang, D., Moy, Y., Wallenburg, A., Chapman, R.: SPARK 2014 and GNATprove: a competition report from builders of an industrial-strength verifying compiler. STTT 17(6), 695–707 (2015)CrossRef

61.

Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580, 583 (1969)CrossRef

62.

Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1, 271–281 (1972)CrossRef

63.

Hoder, K., Kovács, L., Voronkov, A.: Invariant generation in vampire. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 60–64. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19835-9_7CrossRef

64.

Homeier, P.V., Martin, D.F.: A mechanically verified verification condition generator. Comput. J. 38(2), 131–141 (1995)CrossRef

65.

Huisman, M.: Reasoning about Java programs in higher order logic with PVS and Isabelle. Ph.D. thesis, University of Nijmegen (2001)

66.

Huisman, M., Ahrendt, W., Grahl, D., Hentschel, M.: Formal specification with the Java modeling language. In: Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P., Ulbrich, M. (eds.) Deductive Software Verification - The KeY Book. LNCS, vol. 10001, pp. 193–241. Springer, Cham (2016)CrossRef

67.

Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 284–303. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46428-X_20CrossRef

68.

Huisman, M., Monahan, R., Müller, P., Poll, E.: VerifyThis 2016: a program verification competition. Technical report TR-CTIT-16-07, Centre for Telematics and Information Technology, University of Twente, Enschede (2016)

69.

Ireland, A., Jackson, M., Reid, G.: Interactive proof critics. Formal Asp. Comput. 11(3), 302–325 (1999)CrossRef

70.

Jacobs, B.: A formalisation of Java’s exception mechanism. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 284–301. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45309-1_19CrossRef

71.

Jacobs, B., Piessens, F.: Expressive modular fine-grained concurrency specification. In: Ball, T., Sagiv, M. (eds.) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, Austin, TX, USA, pp. 271–282. ACM (2011)

72.

Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_4CrossRef

73.

Jeannin, J., Ghorbal, K., Kouskoulas, Y., Gardner, R., Schmidt, A., Zawadzki, E., Platzer, A.: Formal verification of ACAS X, an industrial airborne collision avoidance system. In: Girault, A., Guan, N. (eds.) International Conference on Embedded Software, EMSOFT, Amsterdam, Netherlands, pp. 127–136. IEEE (2015)

74.

Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142–164. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25271-6_8CrossRef

75.

Jones, C.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596–619 (1983)CrossRef

76.

Kassios, I.T.: The dynamic frames theory. Formal Asp. Comput. 23(3), 267–288 (2011)MathSciNetCrossRef

77.

Kassios, I.T., Müller, P., Schwerhoff, M.: Comparing verification condition generation with symbolic execution: an experience report. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 196–208. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27705-4_16CrossRef

78.

Kaufmann, M., Moore, J.S.: Design goals for ACL2. In: Third International School and Symposium on Formal Techniques in Real Time and Fault Tolerant Systems, pp. 92–117 (1994)

79.

Kiniry, J.R., Morkan, A.E., Cochran, D., Fairmichael, F., Chalin, P., Oostdijk, M., Hubbers, E.: The KOA remote voting system: a summary of work to date. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol. 4661, pp. 244–262. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75336-0_16CrossRef

80.

Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Asp. Comput. 27(3), 573–609 (2015)MathSciNetCrossRef

81.

Kosmatov, N., Marché, C., Moy, Y., Signoles, J.: Static versus dynamic verification in Why3, Frama-C and SPARK 2014. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 461–478. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_32CrossRef

82.

Kovács, L.: Symbolic computation and automated reasoning for program analysis. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 20–27. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33693-0_2CrossRef

83.

Larsson, D., Hähnle, R.: Symbolic fault injection. In: Beckert, B. (ed.) Proceedings of the 4th International Verification Workshop (Verify) in Connection with CADE-21 Bremen, Germany, vol. 259, pp. 85–103. CEUR Workshop Proceedings (2007)

84.

Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. Technical report 98-06y, Iowa State University, Department of Computer Science (2003). Revised June 2004

85.

Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P., Zimmerman, D.M., Dietl, W.: JML Reference Manual, May 2013. Draft revision 2344

86.

Lehner, H., Müller, P.: Formal translation of bytecode into BoogiePL. Electr. Notes Theor. Comput. Sci. 190(1), 35–50 (2007)CrossRef

87.

Leino, K.R.M., Müller, P., Smans, J.: Verification of concurrent programs with Chalice. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 195–222. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03829-7_7CrossRef

88.

Leino, K., Nelson, G., Saxe, J.: ESC/Java user’s manual. Technical report SRC 2000–002, Compaq System Research Center (2000)

89.

Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_20CrossRefMATH

90.

Leino, K.R.M., Nelson, G.: An extended static checker for Modula-3. In: Koskimies, K. (ed.) CC 1998. LNCS, vol. 1383, pp. 302–305. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0026441CrossRef

91.

Leino, K.R.M., Wüstholz, V.: The Dafny integrated development environment. In: Dubois, C., Giannakopoulou, D., Méry, D. (eds.) Proceedings of the 1st Workshop on Formal Integrated Development Environment, F-IDE, Grenoble, France. EPTCS, vol. 149, pp. 3–15 (2014)

92.

Leino, K.R.M., Wüstholz, V.: Fine-grained caching of verification results. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 380–397. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_22CrossRef

93.

Leuschel, M., Falampin, J., Fritz, F., Plagge, D.: Automated property verification for large scale B models with ProB. Formal Asp. Comput. 23(6), 683–709 (2011)MathSciNetCrossRef

94.

Liskov, B., Wing, J.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(1), 1811–1841 (1994)CrossRef

95.

Litvintchouk, S.D., Pratt, V.R.: A proof-checker for dynamic logic. In: Reddy, R. (ed.) Proceedings of the 5th International Joint Conference on Artificial Intelligence, pp. 552–558. William Kaufmann, Cambridge (1977)

96.

Logozzo, F.: Practical verification for the working programmer with CodeContracts and abstract interpretation. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 19–22. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18275-4_3CrossRef

97.

Luckham, D.C., von Henke, F.W.: An overview of Anna, a specification language for Ada. IEEE Softw. 2(2), 9–22 (1985)CrossRef

98.

Marché, C., Paulin-Mohring, C., Urbain, X.: The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML. J. Log. Algebr. Program. 58(1–2), 89–106 (2004)CrossRef

99.

Meyer, B.: Applying “design by contract”. IEEE Comput. 25(10), 40–51 (1992)CrossRef

100.

Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall, Englewood Cliffs (1997)MATH

101.

Mohsen, M., Jacobs, B.: One step towards automatic inference of formal specifications using automated VeriFast. In: ter Beek, M.H., Gnesi, S., Knapp, A. (eds.) FMICS/AVoCS -2016. LNCS, vol. 9933, pp. 56–64. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-45943-1_4CrossRef

102.

Mostowski, W.: Fully verified Java Card API reference implementation. In: Beckert, B. (ed.) Proceedings of the 4th Interenational Verification Workshop in connection with CADE-21, Bremen, Germany. CEUR Workshop Proceedings, vol. 259. CEUR-WS.org (2007)

103.

Mostowski, W.: Dynamic frames based verification method for concurrent Java programs. In: Gurfinkel, A., Seshia, S.A. (eds.) VSTTE 2015. LNCS, vol. 9593, pp. 124–141. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-29613-5_8CrossRef

104.

Müller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41–62. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49122-5_2CrossRefMATH

105.

Norrish, M.: C formalised in HOL. Ph.D. thesis, University of Cambridge (1998)

106.

O’Hearn, P.W.: Resources, concurrency and local reasoning. Theoret. Comput. Sci. 375(1–3), 271–307 (2007)MathSciNetCrossRef

107.

Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatica J. 6, 319–340 (1975)MathSciNetCrossRef

108.

Paganelli, G., Ahrendt, W.: Verifying (in-)stability in floating-point programs by increasing precision, using SMT solving. In: Bjørner, N., Negru, V., Ida, T., Jebelean, T., Petcu, D., Watt, S.M., Zaharie, D. (eds.) 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013, Timisoara, Romania, 23–26 September 2013, pp. 209–216. IEEE Computer Society (2013)

109.

Petiot, G., Kosmatov, N., Botella, B., Giorgetti, A., Julliand, J.: Your proof fails? Testing helps to find the reason. In: Aichernig, B.K.K., Furia, C.A.A. (eds.) TAP 2016. LNCS, vol. 9762, pp. 130–150. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41135-4_8CrossRef

110.

Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebr. Program. 60–61, 17–139 (2004)MathSciNetMATH

111.

Polikarpova, N., Tschannen, J., Furia, C.A.: A fully verified container library. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 414–434. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19249-9_26CrossRef

112.

Praxis Critical Systems. SPARK–The SPADE Ada Kernel, 3.2 edition (1996)

113.

Robinson, K.: The B method and the B toolkit. In: Johnson, M. (ed.) AMAST 1997. LNCS, vol. 1349, pp. 576–580. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0000503CrossRef

114.

Rodríguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci. Comput. Program. 64(1), 54–75 (2007)MathSciNetCrossRef

115.

RTCA. DO-178C, Software Considerations in Airborne Systems and Equipment Certification, January 2012

116.

Schellhorn, G., Ernst, G., Pfähler, J., Haneberg, D., Reif, W.: Development of a verified flash file system. In: Ameur, Y.A., Schewe, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z. LNCS, vol. 8477, pp. 9–24. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-43652-3_2CrossRef

117.

Scheurer, D., Hähnle, R., Bubel, R.: A general lattice model for merging symbolic execution branches. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 57–73. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47846-3_5CrossRef

118.

Steffen, B.: The physics of software tools: SWOT analysis and vision. Softw. Tools Technol. Transf. (STTT) 19(1), 1–7 (2017)CrossRef

119.

Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 43(4), 337–362 (2009)MathSciNetCrossRef

120.

Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N.: AutoProof: auto-active functional verification of object-oriented programs. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 566–580. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_53CrossRef

121.

Turon, A., Vafeiadis, V., Dreyer, D.: GPS: navigating weak memory with ghosts, protocols, and separation. In: Black, A.P., Millstein, T.D. (eds.) Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA, Portland, OR, USA, pp. 691–707. ACM (2014)

122.

Ulbrich, M.: Dynamic logic for an intermediate language: verification, interaction and refinement. Ph.D. thesis, Karlsruhe Institute of Technology (2013)

123.

Vafeiadis, V.: Automatically proving linearizability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 450–464. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_40CrossRef

124.

Vafeiadis, V., Narayan, C.: Relaxed separation logic: a program logic for C11 concurrency. In: OOPSLA 2013. ACM (2013)

125.

Vafeiadis, V., Parkinson, M.: A marriage of rely/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256–271. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74407-8_18CrossRef

126.

von Oheimb, D.: Hoare logic for Java in Isabelle/HOL. Concur. Comput.: Pract. Exp. 13(13), 1173–1214 (2001)CrossRef

127.

Wong, P.Y.H., Albert, E., Muschevici, R., Proença, J., Schäfer, J., Schlatte, R.: The ABS tool suite: modelling, executing and analysing distributed adaptable object-oriented systems. STTT 14(5), 567–588 (2012)CrossRef

Titel: Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools
verfasst von: Reiner Hähnle
Marieke Huisman
Verlag: Springer International Publishing
Buch: Computing and Software Science
Print ISBN: 978-3-319-91907-2

Electronic ISBN: 978-3-319-91908-9

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-319-91908-9_18

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"

Premium Partner