scientific article; zbMATH DE number 3485178
From MaRDI portal
Publication:4068060
Cited in
(61)- Efficient symbolic analysis of programs
- The logic-termal equivalence is polynomial-time decidable
- Tree equivalence of linear recursive schemata is polynomial-time decidable
- Finite constants: Characterizations of a new decidable set of constants
- Program equivalence and context-free grammars
- Node listings for reducible flow graphs
- Profitability computations on program flow graphs
- Äquivalente Transformationen für Flußdiagramme
- Bidirectional data flow analysis for type inferencing.
- Automatic generation of interprocedural data-flow analyzers and optimizers
- On sparse evaluation representations
- Mechanising a type-safe model of multithreaded Java with a verified compiler
- A unifying view on SMT-based software verification
- Demand-driven interprocedural analysis for map-based abstract domains
- Verified bytecode verifiers.
- On the computational complexity of data flow analysis over finite bounded meet semilattices
- A decision tree lifted domain for analyzing program families with numerical features
- Optimizing reversible programs
- Compositional verification of smart contracts through communication abstraction
- A flow-insensitive-complete program representation
- System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory
- Data flow analysis of asynchronous systems using infinite abstract domains
- Instruction-level security analysis for information flow in stack-based assembly languages
- A class of polynomially solvable range constraints for interval analysis without widenings
- A formally verified compiler back-end
- Automated formal analysis and verification: an overview
- Complete abstractions and subclassical modal logics
- Dataflow analysis for datarace-free programs
- Typing local control and state using flow analysis
- The Cayley-Hamilton Theorem for Noncommutative Semirings
- The Birth of Model Checking
- Abstract Interpretation with Applications to Timing Validation
- A scalable segmented decision tree abstract domain
- An algorithm for tracing live variables based on a straightened program graph
- Mechanized verification of computing dominators for formalizing compilers
- A Case Study in Abstract Interpretation Based Program Transformation
- Property-oriented expansion
- An even faster solver for general systems of equations
- Tractable constraints in finite semilattices
- Continualization of probabilistic programs with correction
- Data flow analysis as model checking
- Precise interprocedural dataflow analysis with applications to constant propagation
- Compiling Janus to RSSA
- Program Analysis Using Weighted Pushdown Systems
- Control-flow analysis of function calls and returns by abstract interpretation
- An algorithm for analyzing communicating processes
- Efficient interprocedural data-flow analysis using treedepth and treewidth
- Application of static analyses for state-space reduction to the microcontroller binary code
- Make flows small again: revisiting the flow framework
- Syntactic and semantic soundness of structural dataflow analysis
- Abstract semantic dependency
- Compositional reasoning for non-multicopy atomic architectures
- Precise interprocedural dataflow analysis with applications to constant propagation
- A categorical framework for program semantics and semantic abstraction
- On verifying secret control flow elimination
- A region analysis algorithm for the live variables problem
- Transformational derivation of an improved alias analysis algorithm
- Non-local configuration of component interfaces by constraint satisfaction
- Algebraic program analysis
- Properties of data flow frameworks: A unified model
- Pentagons: a weakly relational abstract domain for the efficient validation of array accesses
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4068060)