Difference between revisions of "Applications"

From The Maude System
Jump to: navigation, search
Line 21: Line 21:
 
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc.  These applications use meta-level, search, and symbolic features.
 
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc.  These applications use meta-level, search, and symbolic features.
  
* Networking security: N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures ([https://zenodo.org/record/5856306#.YgTkifXMLt0 CSF 2022]).
+
* Networking security: N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures ([https://zenodo.org/record/5856306#.YgTkifXMLt0 WLSPB22]).
  
* Distributed databases: SNOW-​Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf TOSEM 2022]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 TASE 2021]).
+
* Distributed databases: SNOW-​Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf L22]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 LL21]).
  
* IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 CCS 19]), Automated Composition, Analysis and Deployment of IoT Applications ([https://doi.org/10.1007/978-3-030-29852-4_21 TOOLS 2019]).
+
* IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 WDYLBG19]), Automated Composition, Analysis and Deployment of IoT Applications ([https://doi.org/10.1007/978-3-030-29852-4_21 DG19]).
  
 
Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es.
 
Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es.

Revision as of 12:26, 10 March 2022

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

  • Semantics of hardware architectures: MCA ARMv8 architecture (XZ22).
  • Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer (CMSWW07), and design and verification of the secure-by-construction Illinois’s IBOS browser (SKMT12, SMR20).
  • Cryptographic protocol analysis: Maude-NPA has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM (GAEMM18), IBM’s CCA (GSEMM14), and PCKS#11 (GSEMM15), using unification and symbolic reachability. Tamarin at ETH, resp. AKISS at INRIA, use Maude’s unification to analyze protocols like 5G-AKA (DC18), resp. RFID (GK17).
  • Cloud transaction system formalization and analysis: Cassandra (LNGRG15), Google’s Megastore (GO14), P-Store (O17), etc. (Betal18), using SMC.
  • Analysis of real-time and cyber-physical systems: CASH scheduling (OC06), sensor (OT09) and MANET (LOM16) networks, timed security protocols (AEMMS20), PALS transformation from synchronous to correct distributed real-time systems (MO12, BMO12) enables model checking of complex models such as AADL and Ptolemy models (BOM14) and distributed control of airplane maneuvers (BKMO12).
  • Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. (Pathway Logic)
  • Specification and analysis of models of Concurrency: Petri Nets (SMO01), CCS, pi-Calculus (S00), Actors (M93), REO (MSA), Orc (AM15).
  • Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube (SM04), linear logic (MM02), modal logics (OPR18), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive (DM12, DMR20) and Reachability Logic (SSM17), theorem provers, HOL-to-Nuprl translator (NSM01), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features.
  • Networking security: N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures (WLSPB22).
  • Distributed databases: SNOW-​Optimal Read Atomic Transactions (L22), Replicated RAMP Transactions (LL21).
  • IoT systems: Attack Surface of Trigger-Action IoT Platforms (WDYLBG19), Automated Composition, Analysis and Deployment of IoT Applications (DG19).

Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es.