{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T12:38:04Z","timestamp":1742992684413,"version":"3.40.3"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030577605"},{"type":"electronic","value":"9783030577612"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,8,18]],"date-time":"2020-08-18T00:00:00Z","timestamp":1597708800000},"content-version":"vor","delay-in-days":230,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-57761-2_5","type":"book-chapter","created":{"date-parts":[[2020,8,31]],"date-time":"2020-08-31T12:47:58Z","timestamp":1598878078000},"page":"94-120","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Flexible Formality Practical Experience with Agile Formal Methods"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9331-1462","authenticated-orcid":false,"given":"Philipp","family":"Kant","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4326-4562","authenticated-orcid":false,"given":"Kevin","family":"Hammond","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7450-4429","authenticated-orcid":false,"given":"Duncan","family":"Coutts","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9036-8252","authenticated-orcid":false,"given":"James","family":"Chapman","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8912-4530","authenticated-orcid":false,"given":"Nicholas","family":"Clarke","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3838-3038","authenticated-orcid":false,"given":"Jared","family":"Corduan","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9462-8584","authenticated-orcid":false,"given":"Neil","family":"Davies","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3588-7468","authenticated-orcid":false,"given":"Javier","family":"D\u00edaz","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1002-6023","authenticated-orcid":false,"given":"Matthias","family":"G\u00fcdemann","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8068-8401","authenticated-orcid":false,"given":"Wolfgang","family":"Jeltsch","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9902-8315","authenticated-orcid":false,"given":"Marcin","family":"Szamotulski","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3271-3841","authenticated-orcid":false,"given":"Polina","family":"Vinogradova","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,8,18]]},"reference":[{"key":"5_CR1","volume-title":"Continuous Testing","author":"W Ariola","year":"2014","unstructured":"Ariola, W., Dunlop, C.: Continuous Testing. CreateSpace Independent Publishing Platform, North Charleston (2014)"},{"key":"5_CR2","unstructured":"Beck, K., et al.: Manifesto for agile software development (2001). \nhttp:\/\/www.agilemanifesto.org\/"},{"key":"5_CR3","volume-title":"Extreme Programming Explained: Embrace Change","author":"K Beck","year":"2000","unstructured":"Beck, K.: Extreme Programming Explained: Embrace Change. Addison-Wesley Longman Publishing Co. Inc., Boston (2000)"},{"key":"5_CR4","unstructured":"Badertscher, C., Gazi, P., Kiayias, A., Russell, A., Zikas, V.: Ouroboros genesis: composable proof-of-stake blockchains with dynamic availability. Cryptology ePrint Archive, Report 2018\/378 (2018). \nhttps:\/\/eprint.iacr.org\/2018\/378"},{"key":"5_CR5","unstructured":"Bruenjes, L., Kiayias, A., Koutsoupias, E., Stouka, A.-P.: Reward sharing schemes for stake pools. Computer Science and Game Theory (cs.GT). \narXiv:1807.11218\n\n (2018)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131\u2013146. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-14052-5_11"},{"key":"5_CR7","unstructured":"Brad, E.: Type-driven Development With Idris. Manning (2016). \nhttp:\/\/www.worldcat.org\/isbn\/9781617293023"},{"key":"5_CR8","volume-title":"Agile Project Management with Kanban","author":"E Brechner","year":"2015","unstructured":"Brechner, E.: Agile Project Management with Kanban, 1st edn. Microsoft Press, Redmond (2015)","edition":"1"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"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 SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1977, pp. 238\u2013252. ACM, New York (1977) . \nhttps:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"5_CR10","volume-title":"Model Checking","author":"EM Clarke Jr","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, ICFP 2000, pp. 268\u2013279. ACM, New York (2000). \nhttps:\/\/doi.org\/10.1145\/351240.351266","DOI":"10.1145\/351240.351266"},{"issue":"1","key":"5_CR12","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s10817-018-9458-4","volume":"61","author":"\u0141 Czajka","year":"2018","unstructured":"Czajka, \u0141., Kaliszyk, C.: Hammer for Coq: automation for dependent type theory. J. Autom. Reason. 61(1), 423\u2013453 (2018). \nhttps:\/\/doi.org\/10.1007\/s10817-018-9458-4","journal-title":"J. Autom. Reason."},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-030-33636-3_10","volume-title":"Mathematics of Program Construction","author":"J Chapman","year":"2019","unstructured":"Chapman, J., Kireev, R., Nester, C., Wadler, P.: System F in Agda, for fun and profit. In: Hutton, G. (ed.) Mathematics of Program Construction. Lecture Notes in Computer Science, vol. 11825, pp. 255\u2013297. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-33636-3_10"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"David, B.M., Gazi, P., Kiayias, A., Russell, A.: Ouroboros Praos: an adaptively-secure, semi-synchronous proof-of-stake protocol. IACR Cryptology ePrint Archive 2017, 573 (2017)","DOI":"10.1007\/978-3-319-78375-8_3"},{"key":"5_CR15","unstructured":"Davies, N., Holyer, J., Stephens, A., Thompson, P.: Generating service level agreements from user requirements. In: The Management and Design of ATM Networks, vol. 5, pp. 4\/1\u20134\/9, December 1999"},{"key":"5_CR16","unstructured":"Davies, N., Holyer, J., Thompson, P.: End-to-end management of mixed applications across networks. In: IEEE Workshop on Internet Applications, pp. 12\u201319. IEEE, September 1999"},{"key":"5_CR17","unstructured":"Davies, N., Holyer, J., Thompson, P.: An operational model to control loss and delay of traffic at a network switch. In: The Management and Design of ATM Networks, vol. 5, pp. 20\/1\u201320\/14, December 1999"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/3-540-45748-8_24","volume-title":"Peer-to-Peer Systems","author":"JR Douceur","year":"2002","unstructured":"Douceur, J.R.: The Sybil attack. In: Druschel, P., Kaashoek, F., Rowstron, A. (eds.) IPTPS 2002. LNCS, vol. 2429, pp. 251\u2013260. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45748-8_24"},{"key":"5_CR20","unstructured":"IOHK Formal Methods Team: Small step semantics for Cardano. IOHK Technical report FM-TR-2018-01 (2018). \nhttps:\/\/github.com\/input-output-hk\/cardano-ledger-specs"},{"key":"5_CR21","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-319-73897-0_2","volume-title":"The Essence of Software Engineering","author":"C Ghezzi","year":"2018","unstructured":"Ghezzi, C.: Formal methods and agile development: towards a happy marriage. The Essence of Software Engineering, pp. 25\u201336. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-73897-0_2"},{"key":"5_CR22","unstructured":"Hi-Lite Team: Hi-Lite - Simplifying the use of formal methods (2013). \nhttp:\/\/www.open-do.org\/wp-content\/uploads\/2013\/05\/hilite-L5.3.pdf"},{"key":"5_CR23","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1147\/sj.331.0089","volume":"33","author":"PA Hausler","year":"1994","unstructured":"Hausler, P.A., Linger, R.C., Trammell, C.J.: Adopting cleanroom software engineering with a phased approach. IBM Syst. J. 33, 89\u2013109 (1994)","journal-title":"IBM Syst. J."},{"key":"5_CR24","unstructured":"IOHK Marlowe Team. \nhttps:\/\/testnet.iohkdev.io\/en\/marlowe\/tools\/marlowe-playground\/"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Jeltsch, W.: A process calculus for formally verifying blockchain consensus protocols. To appear, November 2019. \nhttps:\/\/github.com\/jeltsch\/wflp-2019\/tree\/master\/Paper","DOI":"10.1007\/978-3-030-46714-2_2"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Klein, G., et al.: Sel4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP 2009, pp. 207\u2013220. Association for Computing Machinery, New York (2009). \nhttps:\/\/doi.org\/10.1145\/1629575.1629596","DOI":"10.1145\/1629575.1629596"},{"key":"5_CR27","unstructured":"Karakostas, D., Kiayias, A., Larangeira, M.: Account management and stake pools in proof of stake ledgers (2018)"},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-319-63688-7_12","volume-title":"Advances in Cryptology \u2013 CRYPTO 2017","author":"A Kiayias","year":"2017","unstructured":"Kiayias, A., Russell, A., David, B., Oliynykov, R.: Ouroboros: a provably secure proof-of-stake blockchain protocol. In: Katz, J., Shacham, H. (eds.) CRYPTO 2017. LNCS, vol. 10401, pp. 357\u2013388. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-63688-7_12"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Leon Gaixas, S., et al.: Assuring QoS guarantees for heterogeneous services in RINA networks with $$\\rm \\Delta $$Q. In: IEEE International Conference on Cloud Computing Technology and Science (CloudCom), pp. 584\u2013589. IEEE, December 2016","DOI":"10.1109\/CloudCom.2016.0101"},{"key":"5_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-030-03427-6_27","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice","author":"P Lamela Seijas","year":"2018","unstructured":"Lamela Seijas, P., Thompson, S.: Marlowe: financial contracts on blockchain. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 356\u2013375. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-030-03427-6_27"},{"key":"5_CR31","doi-asserted-by":"publisher","first-page":"08","DOI":"10.1145\/2692915.2628143","volume":"49","author":"D Mulligan","year":"2014","unstructured":"Mulligan, D., Owens, S., Gray, K., Ridge, T., Sewell, P.: Lem: reusable engineering of real-world semantics. ACM SIGPLAN Not. 49, 08 (2014)","journal-title":"ACM SIGPLAN Not."},{"key":"5_CR32","unstructured":"Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system. Cryptography Mailing list, March 2009. \nhttps:\/\/metzdowd.com"},{"key":"5_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-642-22863-6_27","volume-title":"Interactive Theorem Proving","author":"S Owens","year":"2011","unstructured":"Owens, S., B\u00f6hm, P., Zappa Nardelli, F., Sewell, P.: Lem: a lightweight tool for heavyweight semantics. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 363\u2013369. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22863-6_27"},{"key":"5_CR34","unstructured":"Hase, K.-R.: openETCS: model-based, agile and open-source (2016). \nhttp:\/\/www.schienenfahrzeugtagung.at\/download\/PDF2016\/MiV07_Hase.pdf"},{"key":"5_CR35","volume-title":"A Practical Guide to Feature-Driven Development","author":"SR Palmer","year":"2001","unstructured":"Palmer, S.R., Felsing, M.: A Practical Guide to Feature-Driven Development. Pearson Education, London (2001)"},{"key":"5_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-030-33636-3_15","volume-title":"Mathematics of Program Construction","author":"M Peyton Jones","year":"2019","unstructured":"Peyton Jones, M., Gkoumas, V., Kireev, R., MacKenzie, K., Nester, C., Wadler, P.: Unraveling recursion: compiling an IR with recursion to system F. In: Hutton, G. (ed.) MPC 2019. LNCS, vol. 11825, pp. 414\u2013443. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-33636-3_15"},{"key":"5_CR37","volume-title":"Lean Software Development: An Agile Toolkit","author":"M Poppendieck","year":"2003","unstructured":"Poppendieck, M., Poppendieck, T.: Lean Software Development: An Agile Toolkit. Addison-Wesley Longman Publishing Co. Inc., Boston (2003)"},{"key":"5_CR38","unstructured":"Reeve, D.C.: A new blueprint for network QoS. Ph.D. thesis, Computing Laboratory, University of Kent, Canterbury, Kent, UK, August 2003. \nhttp:\/\/www.cs.kent.ac.uk\/pubs\/2003\/1892"},{"key":"5_CR39","volume-title":"Agile Software Development with Scrum","author":"K Schwaber","year":"2001","unstructured":"Schwaber, K., Beedle, M.: Agile Software Development with Scrum, 1st edn. Prentice Hall PTR, Upper Saddle River (2001)","edition":"1"},{"key":"5_CR40","unstructured":"IOHK Formal Methods Team: Design Specification for Delegation and Incentives in Cardano, IOHK Deliverable SL-D1 (2018). \nhttps:\/\/github.com\/input-output-hk\/cardano-ledger-specs"},{"key":"5_CR41","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1017\/S0956796809990293","volume":"20","author":"P Sewell","year":"2010","unstructured":"Sewell, P., et al.: Ott: effective tool support for the working semanticist. J. Funct. Program. 20, 71\u2013122 (2010)","journal-title":"J. Funct. Program."}],"container-title":["Lecture Notes in Computer Science","Trends in Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-57761-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,31]],"date-time":"2020-08-31T13:11:02Z","timestamp":1598879462000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-57761-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030577605","9783030577612"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-57761-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"18 August 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TFP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Trends in Functional Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Krakow","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Poland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 February 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 February 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tfp2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/tfp2020.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"50% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3,21","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3,39","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}