Ragionamento continuo
Il ragionamento continuo (o continuous reasoning, CR) è una metodologia di ragionamento automatico che sfrutta la composizionalità per analizzare sistemi di larga scala in modo differenziale. Il ragionamento continuo si concentra sull'analisi delle ultime modifiche introdotte nel sistema e riutilizza i risultati di analisi precedenti per quanto possibile. L'obiettivo del ragionamento continuo è quello di contenere l'elevata complessità computazionale dei problemi su sistemi di larga scala attraverso la risoluzione di istanze più piccole dei problemi da risolvere, ovvero risolvendo istanze che considerino principalmente ciò che è cambiato nel sistema dopo l'ultima analisi effettuata.
Il ragionamento continuo è stato proposto per primo da O'Hearn[1] nel 2018 e ha ottenuto particolare successo nel supportare lo sviluppo iterativo del software nelle grandi aziende IT con l'impiego di strumenti di ragionamento automatico come Infer di Facebook[2][3] e Amazon s2n[4]. Tali strumenti eseguono analisi statiche incrementali[5] su grandi basi di codice, concentrandosi solo sulle differenze tra una modifica e l'altra, per identificare possibili errori o problemi di sicurezza prima che il codice venga messo in produzione. Recentemente, l'utilizzo del ragionamento continuo è stato proposto anche per la gestione di applicazioni su infrastrutture Fog computing[6].
Note
- ^ (EN) Peter W. O'Hearn, Continuous Reasoning: Scaling the impact of formal methods, in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, ACM, 9 luglio 2018, pp. 13–25, DOI:10.1145/3209108.3209109. URL consultato il 30 settembre 2020.
- ^ (EN) Dino Distefano, Manuel Fähndrich e Francesco Logozzo, Scaling static analyses at Facebook, in Communications of the ACM, vol. 62, n. 8, 24 luglio 2019, pp. 62–70, DOI:10.1145/3338112. URL consultato il 30 settembre 2020.
- ^ (EN) Cristiano Calcagno, Dino Distefano e Jeremy Dubreil, Moving Fast with Software Verification, in NASA Formal Methods, Springer International Publishing, 2015, pp. 3–11, DOI:10.1007/978-3-319-17524-9_1. URL consultato il 30 settembre 2020.
- ^ Andrey Chudnov, Nathan Collins e Byron Cook, Computer Aided Verification, vol. 10982, Springer International Publishing, 2018, pp. 430–446, DOI:10.1007/978-3-319-96142-2_26, ISBN 978-3-319-96141-5. URL consultato il 30 settembre 2020.
- ^ (EN) Helmut Seidl, Julian Erhard e Ralf Vogler, From Lambda Calculus to Cybersecurity Through Program Analysis, vol. 12065, Springer International Publishing, 2020, pp. 132–148, DOI:10.1007/978-3-030-41103-9_5, ISBN 978-3-030-41102-2. URL consultato il 30 settembre 2020.
- ^ Forti, Stefano e Brogi, Antonio, Continuous Reasoning for Managing Next-Gen Distributed Applications, in Proceedings of the 36th International Conference on Logic Programming (ICLP) Technical Communications, EPTCS, vol. 325, 164–177.