位置：成果数据库 > 会议 > 会议详情页
Formal verification of a descent guidance control program of a lunar lander
  • 所属机构名称：北京控制工程研究所
  • 会议名称：19th Conference on Formal Methods
  • 时间：2014.5.12
  • 成果类型：会议
  • 相关项目：航天嵌入式软件可信性保障集成环境和示范验证与应用
同会议论文项目
航天嵌入式软件可信性保障集成环境和示范验证与应用
期刊论文 86 会议论文 82
同项目会议论文
An Empirical Study on the Test Adequacy Criterion Based on Coincidental Correctness Probability
Automatic XACML Requests Generation for Testing Access Control Policies
An Abstract Domain to Infer Octagonal Constraints with Absolute Value
Fault localization based on dynamic slicing via JSlice for Java programs
Aalta: An LTL satisfiability checker over Infinite/Finite traces
Automated Coverage-Driven Test Data Generation Using Dynamic Symbolic Execution
An assume/guarantee based compositional calculus for hybrid CSP
QCSP based Schedulability Test of Real-time System
Modular Heap Abstraction-based Code Clone Detection for Heap-manipulating Programs
UCBench: A user-centric benchmark suite for C code static analyzers
Cryptanalysis of an Implementation of TTM Cryptosystems Based on Q2 k-module
An Approach to Requirement Analysis for Periodic Control Systems
Automatically Discovering Relaxed Lyapunov Functions for Polynomial Dynamical Systems
Unblockable compositions of software components
A type system for SPARDL
MDM: A Mode Diagram Modeling Framework for Periodic Control Systems
On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs wit
Light-Weight Test Oracles for Resource Leaks Based on Finalizers
Graph-Based Object-Oriented Hoare Logic
Combining Symbolic Execution and Model Checking for Data Flow Testing
Dynamically Validating Static Memory Leak Warnings
An Attributes-Based Allocation Approach of Software Trustworthy Degrees
Using automated program repair for evaluating the effectiveness of fault localization techniques
Static analysis of list-manipulating programs via bit-vectors and numerical abstractions
Data race detection for interrupt-driven programs via bounded model checking
Verified error bounds for real solutions of positive-dimensional polynomial systems
Decidability of the reachability for a family of linear vector fields
Automatic stability and safety verification for delay differential equations
Bounded Model-checking of Discrete Duration Calculus
Modular Heap Abstraction-based Memory Leak Detection for Heap-manipulating Programs
Stability of software trustworthiness measurements models
Automatic Detection of Parameter Shielding for Test Case Generation
Error Detection for Floating-Point Program via Branch and Bound Method
A new method for multi-objective optimization problem
Bound-oriented parallel pruning approaches for efficient resource constrained scheduling of high-lev
On the relationship between LTL normal forms and Büchi automata
Making Automatic Repair for Large-scale Programs More Efficient Using Weak Recompilation
Super-dense computation in verification of HCSP processes
Modeling Real-time Scheduling Problem Schedulability Test in QCSP
Branch-and-bound style resource constrained scheduling using efficient structure-aware pruning
Formal modelling, analysis and verification of hybrid systems
Verifying chinese train control system under a combined scenario by theorem proving
Synthesizing switching controllers for hybrid systems by generating invariants
CCMC: A conditional CSL model checker for continuous-time Markov chains
An interface model of software components
PoMMaDe: Pushdown model-checking for Malware detection
Leveraging specifications of subcomponents to mine precise specifications of composite components
Efficient Automated Program Repair through Fault-Recorded Testing Prioritization
Empirical effectiveness evaluation of spectra-based fault localization on automated program repair
A search strategy guided by uncovered branches for concolic testing
Cascade: A test generation tool for combinatorial testing
Optimizing nop-shadows typestate analysis by filtering interferential configurations
A Refinement Calculus for Hybrid Systems
Denial-of-Service Security Attack in the Continuous-Time World
Automatic Test Data Generation for Unit Testing to Achieve MC/DC Criterion
Incremental Semantic LTL Bounded Model Checking
Backward-slice-based statistical fault localization without test oracles
Counterexample-preserving reduction for symbolic model checking
LTLf Satisfiability Checking
Verifying Simulink diagrams via a Hybrid Hoare Logic Prover
Formal verification of Simulink/Stateflow diagrams
Hybrid Annex: An AADL Extension for Continuous Behavior and Cyber-Physical Interaction Modeling
Adding Formal Meanings to AADL Models with Hybrid Annex
A "hybrid" approach for synthesizing optimal controllers of hybrid systems: A case study o
Verifying OO programs by linking algebraic and abstract specifications
Effective statistical fault localization using program slices
Precise pointer analysis for list-manipulating programs based on quantitative separation logic
Static Analysis of List-manipulating Programs via Bit-Vectors and Numerical Abstractions
Safety verification of nonlinear systems based on rational invariants
An Improved HHL Prover: An Interactive Theorem Prover for Hybrid Systems
A Software Trustworthiness Measure Based on the Decompositions of Trustworthy Attributes and Its Val
A quantitative relation model between trustworthy attributes
Forward and backward: Bounded model checking of linear hybrid automata from two directions
Guaranteeing Proper-Temporal-Embedding safety rules in wireless CPS: A hybrid formal modeling approa
Bounded model-checking of discrete duration calculus
Efficient Two-Phase Approaches for Branch-and-Bound Style Resource Constrained Scheduling
Model-Checking for Android Malware Detection
Runtime Verification by Convergent Formula Progression
Generating non-linear interpolants by semi-definite programming
Super-Dense Computation in Verification of Hybrid CSP Processes
Abstraction of elementary hybrid systems by variable transformation