swMATH4216MaRDI QIDQ16399FDOQ16399
Author name not available (Why is that?)
Official website: https://frama-c.com/acsl.html
Cited In (89)
- A Configurable ACSL-Based Interface Generator for Simulated Systems
- Formal verification of side-channel countermeasures using self-composition
- An approach to verifying and debugging simulation models governed by ordinary differential equations: Part 1. Methodology for residual generation
- Nichtlineare Schwingungen mechanischer Strukturen mit Füge‐oder Kontaktstellen
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- THE USE OF FINITE ELEMENT ELECTROMAGNETICS PACKAGES IN UNDERGRADUATE COURSES
- A refinement methodology for object-oriented programs
- The elastic system study of the vibrating mill with spatial motions for milling the metallic powders
- Title not available (Why is that?)
- Abstract contract synthesis and verification in the symbolic \(\mathbb{K}\) framework
- LMS-Verify: abstraction without regret for verified systems programming
- Verifying Whiley programs with Boogie
- A continuous-system simulation language designed for LSI economics
- Towards an institutional framework for heterogeneous formal development in UML -- a position paper
- Formal analysis of the compact position reporting algorithm
- Comparison of numerical solutions of a one-dimensional non-linear heat equation
- Experiments in verification of linear model predictive control: automatic generation and formal verification of an interior point method algorithm
- Applying Formal Methods: Testing, Performance, and M/E-Commerce
- How testing helps to diagnose proof failures
- Advanced Continuous Simulation Language (ACSL)
- Fairness modulo theory: a new approach to LTL software model checking
- Obstructions to special Lagrangian desingularizations and the Lagrangian prescribed boundary problem
- Assertion-based slicing and slice graphs
- Dynamical behaviour of a friction oscillator with simultaneous self and external excitation.
- Moses: modular modelling of physical systems in an object-oriented database
- Refiner: A Problem-Solving Environment for Scientific Simulator Creation
- Modular inference of subprogram contracts for safety checking
- Behavioral interface specification languages
- Control: a perspective
- Credible autocoding of convex optimization algorithms
- Rigorous software development. An introduction to program verification.
- Trusting computations: a mechanized proof from partial differential equations to actual program
- Omola
- MOSES
- Caduceus
- Frama-C
- Alt-Ergo
- cvc3
- Gappa
- Spec#
- OptiML
- PathCrawler
- SANTE
- Verification conditions for source-level imperative programs
- BIFPACK
- PlusCal
- Aligators
- HighSpec
- VeriCool
- SIL
- EPK-fix
- STELLA
- ObjectMath
- RALib
- Atoment
- C-Light
- TreatJS
- KindSpec
- Charge!
- Jessie
- FuncTion
- LTLAutomizer
- Ultimate
- AstraVer
- StaDy
- AUTOSAR
- Bifurcation and stability analysis for a non-smooth friction oscillator
- AddressSanitizer
- KERNELC
- Stepwise refinement of heap-manipulating code in Chalice
- A relational shape abstract domain
- SIL - a simulation language. User's guide
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
- Crack characteristic analysis of multi-fault rotor system based on whirl orbits
- Whiley
- JMLAutoTest
- RustBelt
- Whiteoak
- Abstraction and subsumption in modular verification of C programs
- A bond graph model incorporating sensors, actuators, and vehicle dynamics for developing controllers for vehicle safety
- SoftBound
- Stochastic response of a two DOF articulated tower
- Integrated approach to analysis and verification of imperative programs
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- Digital simulation of a rotating shaft with a transverse crack
This page was built for software: ACSL
