Jakarta

JaKarTa is a toolset for specifying and reasoning about the JavaCard platform. The main ingredients of the toolset are: the JaKarTa Specification Language (JSL), a front-end for producing highly readable executable specifications; the JaKarTa Transformation Kit (JTK), a program to manipulate and transform JSL specifications by abstraction and refinement; the JaKarTa Prover Interface (JPI), a compiler that translates JSL specifications into proof assistants; the JaKarTa Automation Kit (JAK), a toolset to support reasoning about executable specifications within proof assistants. Goal of the work is to derive certified Byte Code Verifiers by abstraction from the specification of the JavaCard Virtual Machine. The tool takes the JavaCard Virtual Machine specification that is developed in Coq - in the context of the CertiCartes project - as input. This is a defensive virtual machine, and by abstraction it can be transformed into a byte code verifier plus an offensive virtual machine.


References in zbMATH (referenced in 18 articles , 1 standard article )

Showing results 1 to 18 of 18.
Sorted by year (citations)

  1. Bertolissi, Clara; Fernández, Maribel: A metamodel of access control for distributed environments: applications and properties (2014)
  2. Sewell, Peter; Nardelli, Francesco Zappa; Owens, Scott; Peskine, Gilles; Ridge, Thomas; Sarkar, Susmit; Strniša, Rok: Ott: effective tool support for the working semanticist (2010)
  3. Besson, Frédéric; Cachera, David; Jensen, Thomas; Pichardie, David: Certified static analysis by abstract interpretation (2009)
  4. Review, A.Systematic: Program transformations for light-weight CPU accounting and control in the Java virtual machine (2008)
  5. Suzuki, Satomi; Caers, Jef: A distance-based prior model parameterization for constraining solutions of spatial inverse problems (2008)
  6. Suzuki, Satomi; Caumon, Guillaume; Caers, Jef: Dynamic data integration for structural modeling: Model screening approach using a distance-based model parameterization (2008)
  7. Harrison, Andrew; Taylor, Ian: The Web services resource framework in a peer-to-peer context (2006)
  8. Barthe, Gilles; Courtieu, Pierre; Dufay, Guillaume; Melo de Sousa, Simão: Tool-assisted specification and verification of typed low-level languages (2005)
  9. Cachera, David; Jensen, Thomas; Pichardie, David; Rusu, Vlad: Extracting a data flow analyser in constructive logic (2005)
  10. Qahman, Khalid; Larabi, Abdelkader; Ouazar, Driss; Naji, Ahmed; Cheng, Alexander H.-D.: Optimal and sustainable extraction of groundwater in coastal aquifers (2005)
  11. Boite, Olivier: Proof reuse with extended inductive types (2004)
  12. Barthe, Gilles; Stratulat, Sorin: Validation of the JavaCard platform with implicit induction techniques (2003)
  13. Barthe, Gilles; Courtieu, Pierre: Efficient reasoning about executable specifications in Coq (2002)
  14. Barthe, Gilles; Courtieu, Pierre; Dufay, Guillaume; de Sousa, Simão Melo: Tool-assisted specification and verification of the JavaCard platform (2002)
  15. Barthe, Gilles; Dufay, Guillaume; Jakubiec, Line; Melo de Sousa, Simão: A formal correspondence between offensive and defensive JavaCard virtual machines (2002)
  16. Sarjon, Defit; Mohd, Noor Md Sap: Association rules using rough set and association rule methods (2002)
  17. Wang, Yanfei; Zhang, Yan-Qing; Belkasim, Saeid; Sunderraman, Raj: Real time fuzzy personalized Web stock information agent (2002)
  18. Barthe, G.; Dufay, G.; Huisman, M.; de Sousa, S.Melo: Jakarta: A toolset for reasoning about JavaCard (2001)