tool_scenarios.lando

// Copyright 2021, 2022, 2023 Galois, Inc.
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//     http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

scenarios Tool Scenarios

Verify Software
Formally verify that software or firmware programs fulfill their
specifications.

Verify Hardware
Formally verify that a hardware design fulfills its specifications.

Formal Equivalence Checking
Formally verify that programs written in different languages (even
across the hardware/software boundary) are equivalent.

Symbolic Testing
Improve the assurance of software using symbolic testing.

Backend Solver Libraries
Provide libraries for symbolic formula representation and solver
interaction.

Binary Analysis
Analyze binaries in a variety of formats and for a host of different
Instruction Set Architectures.

Binary Rewriting
Perform binary analysis and rewriting for a variety of purposes.

Model-Based Test Generation
Automatically generate model-based tests for a software, firmware, or
hardware system.

Specify Semi-Formal Architecture using Natural Language Processing
Specify a systems architectures at a high level leveraging Natural
Language Processing technology.

Concretize Model
Create or generate a new model or an implementation from a semi-formal or formal
model or implementation by adding extra information, typically turning
a denotational property into an operational computation, and guarantee
that the new, refined model behaves identically to the previous,
abstract model.

Abstract Model
Extract formal models---including behavioral and architectural
models---from source code and binaries, and guarantee that all
properties of the abstract model hold for the more concrete model or
implementation.

Define Refinement Relation
Define a pair of functions, an abstraction function L: I->M and
concretization function C: M->I, such that they form a refinement
relation over some property P (roughly, P(c(l(i)))=P(i)) between their
pair of types M and I.

Formally Refine a Semi-formal Architecture
Specify and formally refine a semi-formal architecture.

Product Line Engineering
Specify and reason about product lines of hardware, firmware, and/or
software systems.

Reason about Products
Reason about products derived from product lines, particularly
automatically generated CPUs and SoCs.

Reason about Non-Behavioral Properties
Reason about non-behavioral properties of models or implementations,
such as security proofs of cryptographic algorithms and protocols,
safety and progress properties of concurrent or distributed systems,
information leakage properties of embedded systems and hardware
designs.

Configure Product Line
Make feature selections in a feature model in order to specify the
subset of products from a product line that are of interest.

Fully Configure Product Line
Configure a feature model until no open choices exist, thereby
creating a fully configured feature model that specifies a single
product.