{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:34:59Z","timestamp":1761597299539,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642232824"},{"type":"electronic","value":"9783642232831"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-23283-1_13","type":"book-chapter","created":{"date-parts":[[2011,8,24]],"date-time":"2011-08-24T02:30:27Z","timestamp":1314153027000},"page":"173-193","source":"Crossref","is-referenced-by-count":10,"title":["Computing Preconditions and Postconditions of While Loops"],"prefix":"10.1007","author":[{"given":"Olfa","family":"Mraihi","sequence":"first","affiliation":[]},{"given":"Wided","family":"Ghardallou","sequence":"additional","affiliation":[]},{"given":"Asma","family":"Louhichi","sequence":"additional","affiliation":[]},{"given":"Lamia","family":"Labed Jilani","sequence":"additional","affiliation":[]},{"given":"Khaled","family":"Bsaies","sequence":"additional","affiliation":[]},{"given":"Ali","family":"Mili","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Barnett, M., Rustan Leino, K.: Weakest precondition of unstructured programs. In: Proceedings, Sixth ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, Lisbon, Portugal (2005)","DOI":"10.1145\/1108792.1108813"},{"key":"13_CR2","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Soundness of a purely syntactical formalization of weakest preconditions","author":"R. Berghammer","year":"2000","unstructured":"Berghammer, R.: Soundness of a purely syntactical formalization of weakest preconditions. Electronic Notes in Theoretical Computer Science. Elsevier Science Publisher, Amsterdam (2000)"},{"key":"13_CR3","doi-asserted-by":"publisher","first-page":"544","DOI":"10.1007\/BF01211474","volume":"4","author":"N. Boudriga","year":"1992","unstructured":"Boudriga, N., Elloumi, F., Mili, A.: The lattice of specifications: Applications to a specification methodology. Formal Aspects of Computing\u00a04, 544\u2013571 (1992)","journal-title":"Formal Aspects of Computing"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Brumley, D., Wang, H., Jha, S., Song, D.: Creating vulnerability signatures using weakest preconditions. In: Proceedings, 20th Computer Security Foundations Symposium, Venice, Italy, pp. 311\u2013325 (2007)","DOI":"10.1109\/CSF.2007.17"},{"issue":"8","key":"13_CR5","doi-asserted-by":"publisher","first-page":"713","DOI":"10.1109\/32.879810","volume":"26","author":"A. Cavalcanti","year":"2000","unstructured":"Cavalcanti, A., Naumann, D.: A weakest precondition semantics for refinement of object oriented programs. IEEE Transactions on Software Engineering\u00a026(8), 713\u2013728 (2000)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Costa, M., Castro, M., Zhou, L., Zhang, L., Peinado, M.: Bouncer: Securing software by blocking bad input. In: Proceedings, ACM Symposium on Operating Systems Principles (October 2007)","DOI":"10.1145\/1294261.1294274"},{"issue":"8","key":"13_CR7","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, non dterminacy, and formal derivation of programs. Communications of the ACM\u00a018(8), 453\u2013457 (1975)","journal-title":"Communications of the ACM"},{"key":"13_CR8","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Proceedings, POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2002)","DOI":"10.1145\/503272.503291"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: Generating compact verification conditions. In: Proceedings, Symposium on Principles of Programming Languages (2001)","DOI":"10.1145\/360204.360220"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Gannod, G.C., Cheng, B.H.C.: Strongest postcondition semantics as the formal basis for reverse engineering. In: Proceedings, Second Working Conference on Reverse Engineering, Toronto, Ontario, Canada, pp. 188\u2013197 (1995)","DOI":"10.1109\/WCRE.1995.514707"},{"key":"13_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The Science of programming","author":"D. Gries","year":"1981","unstructured":"Gries, D.: The Science of programming. Springer, Heidelberg (1981)"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Grigore, R., Charles, J., Fairmichael, F., Kiniry, J.: Strongest postcondition of unstructured programs. In: Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs (2009)","DOI":"10.1145\/1557898.1557904"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: Proceedings, PLDI 2008: ACM SIGPLAN 2008 Conference on Programming Languages and their Implementation, Tuscon, AZ (2008)","DOI":"10.1145\/1375581.1375616"},{"issue":"10","key":"13_CR15","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a012(10), 576\u2013583 (1969)","journal-title":"Communications of the ACM"},{"key":"13_CR16","unstructured":"Jager, I., Brumley, D.: Efficient directionless weakest preconditions. Technical Report CMU-CyLab-10-002, Carnegie Mellon University (February 2010)"},{"issue":"6","key":"13_CR17","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/j.ipl.2004.10.015","volume":"93","author":"K.R.M. Leino","year":"2005","unstructured":"Leino, K.R.M.: Efficient weakest preconditions. Information Processing Letters\u00a093(6), 281\u2013288 (2005)","journal-title":"Information Processing Letters"},{"key":"13_CR18","unstructured":"Leino, K.R.: Towards reliable modular programs. Technical report, California Institute of Technology, Pasadena, CA (1995)"},{"key":"13_CR19","unstructured":"Louhichi, A., Mraihi, O., Jilani, L.L., Mili, A.: Invariant assertions, invariant relations and invariant functions. In: Proceedings, 2nd International Workshop on Invariant Generation, York, UK (2009)"},{"key":"13_CR20","volume-title":"A Mathematical Theory of Computation","author":"Z. Manna","year":"1974","unstructured":"Manna, Z.: A Mathematical Theory of Computation. McGraw-Hill, New York (1974)"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Mili, A., Aharon, S., Nadkarni, C.: Mathematics for reasoning about loop. Science of Computer Programming, 989\u20131020 (2009)","DOI":"10.1016\/j.scico.2009.09.009"},{"key":"13_CR22","series-title":"International Series in Computer Sciences","volume-title":"Programming from Specifications","author":"C.C. Morgan","year":"1998","unstructured":"Morgan, C.C.: Programming from Specifications. International Series in Computer Sciences. Prentice Hall, London (1998)"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof carrying code. In: Proceedings, Symposium on Principles of Programming Languages (1997)","DOI":"10.1145\/263699.263712"},{"key":"13_CR24","unstructured":"Rauch, N.: Precondition generation for a Java subset. In: Proceedings, FM-TOOLS 2002: The Fifth Workshop on Tools for System Design and Verification, Reisensberg, Germany (2002)"},{"key":"13_CR25","unstructured":"von Oheimb, D.: Analyzing java in isabelle\/hol: Formalization, type safety, and hoare logic. Technical report, Technische Universitaet Muenchen (2001)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2011"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-23283-1_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,9]],"date-time":"2025-03-09T05:58:17Z","timestamp":1741499897000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-23283-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642232824","9783642232831"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-23283-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}