Hostname: page-component-586b7cd67f-rcrh6 Total loading time: 0 Render date: 2024-11-25T17:17:37.361Z Has data issue: false hasContentIssue false
  • English
  • Français

Postlude: seamless composition and integration – a perspective on formal methods research

Published online by Cambridge University Press:  08 July 2013

AZER BESTAVROS ,
ASSAF KFOURY  and
ANDREI LAPETS
AZER BESTAVROS
Affiliation:
Computer Science Department, Boston University, Boston, Massachusetts 02215, U.S.A. Email: [email protected]; [email protected]; [email protected]
ASSAF KFOURY
Affiliation:
Computer Science Department, Boston University, Boston, Massachusetts 02215, U.S.A. Email: [email protected]; [email protected]; [email protected]
ANDREI LAPETS
Affiliation:
Computer Science Department, Boston University, Boston, Massachusetts 02215, U.S.A. Email: [email protected]; [email protected]; [email protected]
Get access Rights & Permissions [Opens in a new window]

Extract

Have formal methods in computer science come of age? While the contributions to this special issue of Mathematical Structures in Computer Science attest to their importance in the design and analysis of particular software systems, their relevance to the field as a whole is far wider. In recent years, formal methods have become more accessible and easier to use, more directly related to practical problems and more adaptable to imperfect and/or approximate specifications in real-life applications. As a result, they are now a central component of computer-science education and research.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 23 , Special Issue 4: Lightweight and Practical Formal Methods in the Design and Analysis of Safety-Critical Systems , August 2013 , pp. 934 - 943
Copyright
Copyright © Cambridge University Press 2013 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abel, A., Chang, B. and Pfenning, F. (2001) Human-readable machine-verifiable proofs for teaching constructive logic. In: Egly, U., Fiedler, A., Horacek, H. and Schmitt, S. (eds.) PTP '01: IJCAR Workshop on Proof Transformations, Proof Presentations and Complexity of Proofs, Siena, Italy.Google Scholar
Ancona, D. and Zucca, E. (2004) Principal typings for Java-like languages. In: POPL '04: Proceedings of the 31st ACM SIGPLAN–SIGACT symposium on Principles of Programming Languages, ACM 306–317.CrossRefGoogle Scholar
Ancona, D., Damiani, F., Drossopoulou, S. and Zucca, E. (2004) Even more principal typings for Java-like languages. In: ECOOP Workshop on Formal Techniques for Java Programs.CrossRefGoogle Scholar
Asperti, A., Coen, C. S., Tassi, E. and Zacchiroli, S. (2007) User interaction with the Matita proof assistant. Journal of Automated Reasoning 39 (2)109–139.CrossRefGoogle Scholar
Aydin, H., Melhem, R. and Moss, D. (2001) Determining optimal processor speeds for periodic real-time tasks with different power characteristics. In: Proceedings of EuroMicro Conference on Real-Time Systems 225–232.CrossRefGoogle Scholar
Bestavros, A. and Kfoury, A. (2011) A Domain-Specific Language for Incremental and Modular Design of Large-Scale Verifiably-Safe Flow Networks. In: Proceedings of IFIP Working Conference on Domain-Specific Languages (DSL 2011). Electronic Proceedings in Theoretical Computer Science 66 24–47.CrossRefGoogle Scholar
Brown, C. E. (2006) Verifying and Invalidating Textbook Proofs using Scunak. In: Borwein, J. M. and Farmer, W. M. (eds.) Mathematical Knowledge Management: Proceedings 5th International Conference, MKM 2006. Springer-Verlag Lecture Notes in Computer Science 4108 110–123.CrossRefGoogle Scholar
Buss, S. R., Kechris, A. S., Pillay, A. and Shore, R. A. (2001) The prospects for mathematical logic in the twenty-first century. The Bulletin of Symbolic Logic 7 (2)169–196.CrossRefGoogle Scholar
Cairns, P. and Gow, J. (2007) Integrating Searching and Authoring in Mizar. Journal of Automated Reasoning 39 (2)141–160.CrossRefGoogle Scholar
Carlier, S., Polakow, J., Wells, J. B. and Kfoury, A. J. (2004) System E: Expansion variables for flexible typing with linear and non-linear types and intersection types. In: Schmidt, D. (ed.) Programming Languages and Systems: 13th European Symposium on Programming, ESOP 2004. Springer-Verlag Lecture Notes in Computer Science 2986 294–309.CrossRefGoogle Scholar
Chklovski, T. (2005) Towards managing knowledge collection from volunteer contributors. In: Proceedings of AAAI Spring Symposium on Knowledge Collection from Volunteer Contributors (KCVC05), AAAI.Google Scholar
Chklovski, T. and Gil, Y. (2005) Improving the design of intelligent acquisition interfaces for collecting world knowledge from web contributors. In: K-CAP '05: Proceedings of the 3rd international conference on Knowledge capture, ACM 35–42.CrossRefGoogle Scholar
Clarke, E. M. and Wing, J. M. (1996) Formal methods: State of the art and future directions. ACM Computing Surveys 28 (4).CrossRefGoogle Scholar
Davis, M. (1988) Influences of mathematical logic on computer science. In: Herkin, R. (ed.) The Universal Turing Machine: A Half-Century Survey, Oxford University Press 315–326.Google Scholar
Deng, Z. and Liu, J. W.-S. (1997) Scheduling real-time applications in an open environment. In: Proceedings of the 18th IEEE Real-Time Systems Symposium, IEEE Computer Society Press 308–319.CrossRefGoogle Scholar
Grumberg, O. and Long, D. E. (1991) Model checking and modular verification. ACM Transactions on Programming Languages and Systems 16 (3)843–871.CrossRefGoogle Scholar
Halpern, J. Y., Harper, R., Immerman, N., Kolaitis, P. G., Vardi, M. Y. and Vianu, V. (2001) On the unusual effectiveness of logic in computer science. The Bulletin of Symbolic Logic 7 (2)213–236.CrossRefGoogle Scholar
Han, S., Wallace, D. R. and Miller, R. C. (2009) Code completion from abbreviated input. In: ASE '09: Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering, IEEE Computer Society 332–343.CrossRefGoogle Scholar
Hanenberg, S. (2009) Costs of using untyped programming languages – first empirical results. In: 13th IFAC Symposium on Information Control Problems in Manufacturing (Track Advanced Software Engineering), Moscow, Russia.Google Scholar
Hanenberg, S. (2010a) Doubts about the positive impact of static type systems on programming tasks in single developer projects – an empirical study. In: D'Hondt, T. (ed.) ECOOP 2010 – Object-Oriented Programming: Proceedings 24th European Conference. Springer-Verlag Lecture Notes in Computer Science 6183 300–303.CrossRefGoogle Scholar
Hanenberg, S. (2010b) Faith, hope, and love – a criticism of software science's carelessness with regard to the human factor. In: Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA/SPLASH) 933–946.CrossRefGoogle Scholar
Hsiung, P.-A. and Cheng, S.-Y. (2003) Automating formal modular verification of asynchronous real-time embedded systems. In: VLSI Design, 2003, Proceedings, 16th International Conference 249–254.CrossRefGoogle Scholar
Jackson, D. (2006) Software Abstractions: Logic, Language, and Analysis, The MIT Press.Google Scholar
Jim, T. (1995) What are principal typings and what are they good for? Technical Memorandum MIT LCS TM 532.CrossRefGoogle Scholar
Kamareddine, F. and Wells, J. B. (2008) Computerizing Mathematical Text with MathLang. Electronic Notes in Theoretical Computer Science 205 5–30.CrossRefGoogle Scholar
Katayama, S. (2006) Library for systematic search for expressions. In AIC '06: Proceedings of the 6th WSEAS International Conference on Applied Informatics and Communications, World Scientific and Engineering Academy and Society (WSEAS) 381–387.Google Scholar
Kfoury, A. (2011) The Denotational, Operational, and Static Semantics of a Domain-Specific Language for the Design of Flow Networks. In: Proceedings of SBLP 2011: Brazilian Symposium on Programming Languages.Google Scholar
Kfoury, A. J. and Wells, J. B. (2004) Principality and type inference for intersection types using expansion variables. Theoretical Computer Science 311 (1–3)1–70.CrossRefGoogle Scholar
Krafzig, D., Banke, K. and Slama, D. (2004) Enterprise SOA: Service-Oriented Architecture Best Practices (The Coad Series), Prentice Hall.Google Scholar
Lapets, A. and Kfoury, A. (2010) A User-friendly Interface for a Lightweight Verification System. In: Proceedings of UITP'10: 9th International Workshop On User Interfaces for Theorem Provers. Electronic Notes in Theoretical Computer Science 285 29–41.CrossRefGoogle Scholar
Li, H. C., Krishnamurthi, S. and Fisler, K. (2005) Modular verification of open features using three-valued model checking. Automated Software Engineering 12 (3)349–382.CrossRefGoogle Scholar
Lim, S.-S.et al. (1995) An accurate worst case timing analysis for risc processors. In: Proceedings of the 15th IEEE real-time systems symposium 97–108.Google Scholar
Little, G. and Miller, R. C. (2007) Keyword programming in Java. In: ASE '07: Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering, ACM 84–93.CrossRefGoogle Scholar
Liu, H. and Singh, P. (2004) Conceptnet – a practical commonsense reasoning tool-kit. BT Technology Journal 22 (4)211–226.CrossRefGoogle Scholar
McMath, D., Rozenfeld, M. and Sommer, R. (2001) A Computer Environment for Writing Ordinary Mathematical Proofs. In: Nieuwenhuis, R. and Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning: Proceedings 8th International Conference, LPAR 2001. Springer-Verlag Lecture Notes in Computer Science 2250 507–516.CrossRefGoogle Scholar
Mitchell, N. (2008) Hoogle overview. The Monad.Reader 12 27–35.Google Scholar
Panton, K.et al. (2006) Common Sense Reasoning – From Cyc to Intelligent Assistant. In: Cai, Y. and Abascal, J. (eds.) Ambient Intelligence in Everyday Life. Springer-Verlag Lecture Notes in Computer Science 3864 1–31.CrossRefGoogle Scholar
Pouwelse, J., Langendoen, K. and Sips, H. (2001) Dynamic voltage scaling on a low-power microprocessor. In: Mobile Computing and Networking – Mobicom 251–259.CrossRefGoogle Scholar
Regehr, J. (2002) Inferring scheduling behavior with Hourglass. In: Proceedings of the FREENIX Track: 2002 USENIX Annual Technical Conference, USENIX Association 143–156.Google Scholar
Saiedian, H. (ed.) (1996) An invitation to formal methods. A ‘roundtable’ of short articles by several authors. IEEE Computer 29 (4)16–30.Google Scholar
Schmidt, D. C., Levine, D. L. and Mungee, S. (1998) The design of the TAO real-time object request broker. Computer Communications 21 294–324.CrossRefGoogle Scholar
Siekmann, J. H., Benzmüller, C., Fiedler, A., Meier, A. and Pollet, M. (2002) Proof Development with OMEGA: sqrt(2) Is Irrational. In: Baaz, M. and Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning 9th International Conference, LPAR 2002. Springer-Verlag Lecture Notes in Computer Science 2514 367–387.CrossRefGoogle Scholar
Soule, N., Bestavros, A., Kfoury, A. and Lapets, A. (2011) Safe Compositional Equation-based Modeling of Constrained Flow Networks. In: Cellier, F. E., Broman, D., Fritzson, P. and Lee, E. A. (eds.) Proceedings of EOOLT 2011: 4th International Workshop on Equation-Based Object-Oriented Modeling Languages and Tools, Linköping University Electronic Press.Google Scholar
Stankovic, J. A. (2000) Vest: A toolset for constructing and analyzing component based embedded systems. In: Henzinger, T. A. and Kirsch, C. M. (eds.) Embedded Software: Proceedings First International Workshop, EMSOFT 2001. Springer-Verlag Lecture Notes in Computer Science 2211 390–402.CrossRefGoogle Scholar
Verchinine, K., Lyaletski, A., Paskevich, A. and Anisimov, A. (2008) On Correctness of Mathematical Texts from a Logical and Practical Point of View. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M. and Wiedijk, F. (eds.) Intelligent Computer Mathematics – Proceedings: 9th International Conference, AISC 2008; 15th Symposium, Calculemus 2008; and 7th International Conference, MKM 2008. Springer-Verlag Lecture Notes in Computer Science 5144 583–598.CrossRefGoogle Scholar
Woodcock, J., Larsen, P. G., Bicarregui, J. and Fitzgerald, J. (2009) Formal methods: Practice and experience. ACM Computing Surveys 41 (4) 19:1–19:36.CrossRefGoogle Scholar