LLVM

swMATH4892MaRDI QIDQ17043FDOQ17043

Author name not available (Why is that?)

Cited In (72)

• Facilitating the design of fault tolerance in transaction level SystemC programs
• Extracting verified decision procedures: DPLL and Resolution
• Enhancing \texttt{R} with advanced compilation tools and methods
• A resource semantics and abstract machine for \textit{Safe}: a functional language with regions and explicit deallocation
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Memory-centric scheduling for multicore hard real-time systems
• Checking data-race freedom of GPU kernels, compositionally
• Fast computation of strong control dependencies
• CScout: a refactoring browser for C
• Sound Bit-Precise Numerical Domains
• On the implementation of GNU Prolog
• A complete semantics of \(\mathbb{K}\) and its translation to Isabelle
• From Under-Approximations to Over-Approximations and Back
• Formalizing the SAFECode Type System
• Julia: A Fresh Approach to Numerical Computing
• Symbolic computation via program transformation
• A matrix-free isogeometric Galerkin method for Karhunen-Loève approximation of random fields using tensor product splines, tensor contraction and interpolation based quadrature
• Programmable program synthesis
• Improving the results of program analysis by abstract interpretation beyond the decreasing sequence
• RSSA: A Reversible SSA Form
• Towards satisfiability modulo parametric bit-vectors
• Lingva: Generating and Proving Program Properties Using Symbol Elimination
• A profile-based tool for finding pipeline parallelism in sequential programs
• Computing in Operations Research Using Julia
• Non-linear Boltzmann equation on hybrid-unstructured non-conforming multi-domains
• Refinement through restraint: bringing down the cost of verification
• Julia language in machine learning: algorithms, applications, and open issues
• Modular Verification of Procedure Equivalence in the Presence of Memory Allocation
• Complexity and resource bound analysis of imperative programs using difference constraints
• Speculative parallelization of sequential loops on multicores
• Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution
• Backward symbolic execution with loop folding
• Hash consed points-to sets
• A formal semantics of the GraalVM intermediate representation
• Whale: An Interpolation-Based Algorithm for Inter-procedural Verification
• In search of a program generator to implement generic transformations for high-performance computing
• A Modern Look at GRIN, an Optimizing Functional Language Back End
• An Abstract Domain of Uninterpreted Functions
• LCTD: test-guided proofs for C programs on LLVM
• Trace-based schedulability analysis to enhance passive side-channel attack resilience of embedded software
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Title not available (Why is that?)
• Extending R
• JuMP: A Modeling Language for Mathematical Optimization
• A new abstraction framework for affine transformers
• Software obfuscation with non-linear mixed Boolean-arithmetic expressions
• A formal approach to the WCRT analysis of multicore systems with memory contention under phase-structured task sets
• Towards bit-width-independent proofs in SMT solvers
• Title not available (Why is that?)
• Structural Abstraction of Software Verification Conditions
• Harnessing static analysis to help learn pseudo-inverses of string manipulating procedures for automatic test generation
• Leveraging compiler intermediate representation for multi- and cross-language verification
• A principled, complete, and efficient representation of C++
• Time-triggered runtime verification
• Program synthesis for interactive-security systems
• Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution
• Relational program reasoning using compiler IR
• CasADi: a software framework for nonlinear optimization and optimal control
• A compiler for MSVL and its applications
• Verification of Concurrent Programs on Weak Memory Models
• Using Fault Screeners for Software Error Detection
• Parallelizing computation of expected values in recombinant binomial trees
• Title not available (Why is that?)
• A Domain-Specific Language and Editor for Parallel Particle Methods
• On the Correctness of the SIMT Execution Model of GPUs
• Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption
• Parallel Assertions for Architectures with Weak Memory Models
• Constraint-based Diversification of JOP Gadgets
• Quo Vadis Explicit-State Model Checking
• A Fast Verified Liveness Analysis in SSA Form
• Title not available (Why is that?)
• Spinsim: a GPU optimized Python package for simulating spin-half and spin-one quantum systems

This page was built for software: LLVM