Extracting a Data Flow Analyser in Constructive Logic

This publication has 10 references indexed in Scilit:

• The synthesis of a Java card tokenisation algorithm
  Published by Institute of Electrical and Electronics Engineers (IEEE) ,2005
• Operational semantics of the Java Card Virtual Machine
  The Journal of Logic and Algebraic Programming, 2004
• Formal development of an embedded verifier for Java Card byte code
  Published by Institute of Electrical and Electronics Engineers (IEEE) ,2003
• Automatically proving the correctness of compiler optimizations
  Published by Association for Computing Machinery (ACM) ,2003
• Verified bytecode verifiers
  Theoretical Computer Science, 2003
• Jakarta: A Toolset for Reasoning about JavaCard
  Published by Springer Nature ,2001
• Formalizing a JVML Verifier for Initialization in a Theorem Prover
  Published by Springer Nature ,2001
• A Formal Executable Semantics of the JavaCard Platform
  Published by Springer Nature ,2001
• Flow logics for constraint based analysis
  Published by Springer Nature ,1998
• Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints
  Published by Association for Computing Machinery (ACM) ,1977