↓ Skip to main content

FM 2016: Formal Methods

Overview of attention for book
Cover of 'FM 2016: Formal Methods'

Table of Contents

  1. Altmetric Badge
    Book Overview
  2. Altmetric Badge
    Chapter 1 Industrial-Strength Model-Based Testing of Safety-Critical Systems
  3. Altmetric Badge
    Chapter 2 Counter-Example Guided Program Verification
  4. Altmetric Badge
    Chapter 3 Tighter Reachability Criteria for Deadlock-Freedom Analysis
  5. Altmetric Badge
    Chapter 4 Compositional Parameter Synthesis
  6. Altmetric Badge
    Chapter 5 Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor
  7. Altmetric Badge
    Chapter 6 A Model Checking Approach to Discrete Bifurcation Analysis
  8. Altmetric Badge
    Chapter 7 State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI
  9. Altmetric Badge
    Chapter 8 Formal Verification of Multi-Paxos for Distributed Consensus
  10. Altmetric Badge
    Chapter 9 Validated Simulation-Based Verification of Delayed Differential Dynamics
  11. Altmetric Badge
    Chapter 10 Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation
  12. Altmetric Badge
    Chapter 11 From Electrical Switched Networks to Hybrid Automata
  13. Altmetric Badge
    Chapter 12 Danger Invariants
  14. Altmetric Badge
    Chapter 13 Local Planning of Multiparty Interactions with Bounded Horizons
  15. Altmetric Badge
    Chapter 14 Finding Suitable Variability Abstractions for Family-Based Analysis
  16. Altmetric Badge
    Chapter 15 Recovering High-Level Conditions from Binary Programs
  17. Altmetric Badge
    Chapter 16 Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations
  18. Altmetric Badge
    Chapter 17 Exploring Model Quality for ACAS X
  19. Altmetric Badge
    Chapter 18 Learning Moore Machines from Input-Output Traces
  20. Altmetric Badge
    Chapter 19 Modal Kleene Algebra Applied to Program Correctness
  21. Altmetric Badge
    Chapter 20 Mechanised Verification Patterns for Dafny
  22. Altmetric Badge
    Chapter 21 Formalising and Validating the Interface Description in the FMI Standard
  23. Altmetric Badge
    Chapter 22 An Algebra of Synchronous Atomic Steps
  24. Altmetric Badge
    Chapter 23 Error Invariants for Concurrent Traces
  25. Altmetric Badge
    Chapter 24 An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for the LEON3 Processor
  26. Altmetric Badge
    Chapter 25 Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow
  27. Altmetric Badge
    Chapter 26 A Generic Logic for Proving Linearizability
  28. Altmetric Badge
    Chapter 27 Refactoring Refinement Structure of Event-B Machines
  29. Altmetric Badge
    Chapter 28 Towards Concolic Testing for Hybrid Systems
  30. Altmetric Badge
    Chapter 29 Explaining Relaxed Memory Models with Program Transformations
  31. Altmetric Badge
    Chapter 30 SpecCert: Specifying and Verifying Hardware-Based Security Enforcement
  32. Altmetric Badge
    Chapter 31 Automated Verification of Timed Security Protocols with Clock Drift
  33. Altmetric Badge
    Chapter 32 Dealing with Incompleteness in Automata-Based Model Checking
  34. Altmetric Badge
    Chapter 33 Equivalence Checking of a Floating-Point Unit Against a High-Level C Model
  35. Altmetric Badge
    Chapter 34 Battery-Aware Scheduling in Low Orbit: The GomX–3 Case
  36. Altmetric Badge
    Chapter 35 Discounted Duration Calculus
  37. Altmetric Badge
    Chapter 36 Sound and Complete Mutation-Based Program Repair
  38. Altmetric Badge
    Chapter 37 An Implementation of Deflate in Coq
  39. Altmetric Badge
    Chapter 38 Decoupling Abstractions of Non-linear Ordinary Differential Equations
  40. Altmetric Badge
    Chapter 39 Regression Verification for Unbalanced Recursive Functions
  41. Altmetric Badge
    Chapter 40 Automated Mutual Explicit Induction Proof in Separation Logic
  42. Altmetric Badge
    Chapter 41 Finite Model Finding Using the Logic of Equality with Uninterpreted Functions
  43. Altmetric Badge
    Chapter 42 GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking
  44. Altmetric Badge
    Chapter 43 Approximate Bisimulation and Discretization of Hybrid CSP
  45. Altmetric Badge
    Chapter 44 A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems
  46. Altmetric Badge
    Chapter 45 Model-Based Design of an Energy-System Embedded Controller Using Taste
  47. Altmetric Badge
    Chapter 46 Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems
  48. Altmetric Badge
    Chapter 47 Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller
  49. Altmetric Badge
    Chapter 48 Taming Interrupts for Verifying Industrial Multifunction Vehicle Bus Controllers
  50. Altmetric Badge
    Chapter 49 Rule-Based Incremental Verification Tools Applied to Railway Designs and Regulations
  51. Altmetric Badge
    Chapter 50 RIVER: A Binary Analysis Framework Using Symbolic Execution and Reversible x86 Instructions
  52. Altmetric Badge
    Chapter 51 Erratum to: Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems
Attention for Chapter 41: Finite Model Finding Using the Logic of Equality with Uninterpreted Functions
Altmetric Badge

Citations

dimensions_citation
3 Dimensions

Readers on

mendeley
5 Mendeley
You are seeing a free-to-access but limited selection of the activity Altmetric has collected about this research output. Click here to find out more.
Chapter title
Finite Model Finding Using the Logic of Equality with Uninterpreted Functions
Chapter number 41
Book title
FM 2016: Formal Methods
Published in
Lecture notes in computer science, November 2016
DOI 10.1007/978-3-319-48989-6_41
Book ISBNs
978-3-31-948988-9, 978-3-31-948989-6
Authors

Amirhossein Vakili, Nancy A. Day

Editors

John Fitzgerald, Constance Heitmeyer, Stefania Gnesi, Anna Philippou

Mendeley readers

Mendeley readers

The data shown below were compiled from readership statistics for 5 Mendeley readers of this research output. Click here to see the associated Mendeley record.

Geographical breakdown

Country Count As %
Unknown 5 100%

Demographic breakdown

Readers by professional status Count As %
Student > Master 3 60%
Student > Ph. D. Student 1 20%
Unknown 1 20%
Readers by discipline Count As %
Computer Science 4 80%
Unknown 1 20%