# Difference between revisions of "Applications"

From The Maude System

(Created page with "Maude and its formal tools have been used in many pioneering applications: • Formal definition and verification of programming and hardware, resp. software, modeling langu...") |
|||

Line 1: | Line 1: | ||

Maude and its formal tools have been used in many pioneering applications: | Maude and its formal tools have been used in many pioneering applications: | ||

− | + | * Formal definition and verification of programming and hardware, resp. software, modeling languages: full C, Java, JVM, NASA’s PLEXIL, Verilog, E-LOTOS, UML, MOF, AADL, and Ptolemy. | |

− | + | * Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer, and design and verification of the secure-by-construction Illinois’s IBOS browser. | |

− | + | * Cryptographic protocol analysis: Maude-NPA has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM, IBM’s CCA, and PCKS#11, using unification and symbolic reachability. Tamarin uses Maude’s unification and has analyzed many important protocols like 5G-AKA. | |

− | + | * Network protocols: AER/NCA active networks, MANETS, BGP; DDoS-Intruder models; and DDoS protection: ASV, Stable Availability, VoIP-SIP, using Maude’s statistical model checking (SMC) tool. | |

− | + | * Cloud transaction system formalization and analysis: Cassandra, Google’s Megastore, P-Store, etc., using SMC. | |

− | + | * Analysis of real-time and cyber-physical systems: CASH scheduling, sensor and MANET networks, timed security protocols, PALS transformation from synchronous to correct distributed real-time systems enables model checking of complex models such as AADL and Ptolemy models and distributed control of airplane maneuvers. | |

− | + | * Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. | |

− | + | * Specification and analysis of models of Concurrency: Petri Nets, CCS, pi-Calculus, Actors, REO, Orc. | |

− | + | * Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube, linear logic, modal logics, computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive and Reachability Logic theorem provers, HOL-to-Nuprl translator, integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features. |

## Revision as of 22:17, 15 December 2020

Maude and its formal tools have been used in many pioneering applications:

- Formal definition and verification of programming and hardware, resp. software, modeling languages: full C, Java, JVM, NASA’s PLEXIL, Verilog, E-LOTOS, UML, MOF, AADL, and Ptolemy.
- Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer, and design and verification of the secure-by-construction Illinois’s IBOS browser.
- Cryptographic protocol analysis: Maude-NPA has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM, IBM’s CCA, and PCKS#11, using unification and symbolic reachability. Tamarin uses Maude’s unification and has analyzed many important protocols like 5G-AKA.
- Network protocols: AER/NCA active networks, MANETS, BGP; DDoS-Intruder models; and DDoS protection: ASV, Stable Availability, VoIP-SIP, using Maude’s statistical model checking (SMC) tool.
- Cloud transaction system formalization and analysis: Cassandra, Google’s Megastore, P-Store, etc., using SMC.
- Analysis of real-time and cyber-physical systems: CASH scheduling, sensor and MANET networks, timed security protocols, PALS transformation from synchronous to correct distributed real-time systems enables model checking of complex models such as AADL and Ptolemy models and distributed control of airplane maneuvers.
- Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc.
- Specification and analysis of models of Concurrency: Petri Nets, CCS, pi-Calculus, Actors, REO, Orc.
- Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube, linear logic, modal logics, computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive and Reachability Logic theorem provers, HOL-to-Nuprl translator, integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features.