About the LaboratoryResearch in the Formal Methods and Declarative Languages Laboratory spans several areas, including: design and implementation of multi-paradigm declarative languages, formal specification and verification, formal tools, logical foundations, and applications to software engineering, distributed systems, and high-assurance systems. The long-term goal is to make programming a much simpler and scientifically-based discipline, and to greatly increase the quality and reliability of systems. Technically, a unifying theme is the use of computational logics as the mathematical basis of declarative languages, so that a program is exactly a theory in a suitable computational logic, and computation is efficient logical deduction. The goal is to develop computational logics that can naturally support concurrent, multi-paradigm programming and a wide range of applications. Rewriting logic is the current computational logic on which the Maude language is based. Having programs as mathematical theories makes much easier reasoning about them and verifying different properties. Such properties can be specified in different logics, such as first-order logic or temporal logic. Maude has an environment of formal verification tools supporting reasoning in both first-order logic and temporal logic. Current application areas include: specification and verification of fault-tolerant and secure network protocols, reflective middleware, mobile systems and languages, probabilistic distributed systems, real-time systems, and automated formal analysis methods and tools for software.Projects
Members
Former Members
PublicationsSome of the publications are currently available on the Maude web-pageLinks
|