Executable computational logics: Combining formal methods and programming language based system design

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

An executable computational logic can provide the desired bridge between formal system properties and formal methods to verify them on the one hand, and executable models of system designs based on programming languages on the other. However, not all such logics are equally well suited for the task. This paper gives some requirements that seem important for a computational logic to be suitable in practice, and discusses the experience with rewriting logic, its Maude language implementation, and its formal tool environment, concluding that they seem to meet well those requirements.

Original languageEnglish (US)
Title of host publicationProceedings - 1st ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE 2003
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages3-9
Number of pages7
ISBN (Electronic)0769519237, 9780769519234
DOIs
StatePublished - 2003
Event1st ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE 2003 - Mont Saint-Michel, France
Duration: Jun 24 2003Jun 26 2003

Publication series

NameProceedings - 1st ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE 2003

Other

Other1st ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE 2003
Country/TerritoryFrance
CityMont Saint-Michel
Period6/24/036/26/03

Keywords

  • Bridges
  • Computer languages
  • Computer science
  • Convergence
  • Hardware
  • Logic design
  • Logic programming
  • Mathematical model
  • Mathematics
  • Military computing

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Hardware and Architecture
  • Electrical and Electronic Engineering

Fingerprint

Dive into the research topics of 'Executable computational logics: Combining formal methods and programming language based system design'. Together they form a unique fingerprint.

Cite this