• Stars
    star
    103
  • Rank 323,280 (Top 7 %)
  • Language
    C++
  • Created about 10 years ago
  • Updated almost 2 years ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

Library for rigorous verification of non-linear arithmetic

Kodiak, a C++ Library for Rigorous Branch and Bound Computation

Kodiak is a C++ library that implements a generic branch and bound algorithm for rigorous numerical approximations. Particular instances of the branch and bound algorithm allow the user to refine and isolate solutions to systems of nonlinear equations and inequalities, global optimization problems, and bifurcation sets for systems of ODEs. Kodiak utilizes interval arithmetic (via the filib++ library) and Bernstein enclosure (for polynomials and rational functions) as self-validating enclosure methods. Symbolic operations support procedures such as automatic partial differentiation.

Maintainers

Marco A. Feliu ([email protected]), National Institute of Aerospace

Aaron M. Dutle ([email protected]), NASA Langley Research Center, US.

Previous Contributors

Cesar A. Munoz, formerly at NASA Langley Research Center, US.

Andrew P. Smith, formerly at National Institute of Aerospace, US.

Anthony Narkawicz, formerly at NASA Langley Research Center, US.

Mantas Markevicius, formerly at University of York, UK.

Documentation

Currently, the main documentation is contained in this file. Publications concerning the library and associated algorithms are in preparation. There are also numerous comments in the source code.

Support and Contribution

See the instructions in this file and the linked resources. For further assistance, or to report problems and bugs, please contact the authors. Contributions to the library are welcomed.

Obtaining Kodiak

The repository is located at: https://github.com/nasa/Kodiak/

License

The Kodiak C++ Library is released under NASA's Open Source Agreement. See the files LICENSES/Kodiak-NOSA.pdf and LICENSES/Kodiak-BooleanChecker-NOSA.pdf; see also the copyright notice at the end of this file.

Installation and Usage Options

Kodiak is installed from source code. Kodiak is run by encoding a problem in a C++ program file, then compiling and running it.

2. Prerequisites

It is recommended to run Kodiak on a Linux or Mac computer with the GNU C++ compiler; so far it has been successfully tested on Ubuntu Linux and Mac OS X. Use of Windows is not supported, although it ought to be feasible, and the authors would welcome any report of successfully running the software on Windows or any other system.

The following software should firstly be installed, if not already present (please follow the links for instructions and support):

  • C++ compiler (standard >=C++14 required)

  • CMake build tool (version >=3.12 required)

  • filib++ interval library (version 3.0.2 required) configured with the following options:

    $ ./configure CFLAGS=-fPIC CPPFLAGS=-fPIC CXXFLAGS=-fPIC
    

    before invoking the make commands:

    $ make
    $ make install
    
  • Boost libraries (only for debugging): http://www.boost.org/users/download/ In addition to the headers, you need at least the library serialization.

2. Build Library and Examples

If necessary, unzip the zip file in order to extract the files. The following files and directories should be present:

  • In the working directory: this README.md file and a CMakeListst.txt file
  • LICENSES: licenses and copyrights for Kodiak
  • logo: Kodiak's logo and credits
  • src: source code for the library
  • examples: example C++ files (.cpp) containing several problems

If any of the prerequisite libraries were installed in non-standard directories, then the file CMakeLists.txt should be modified accordingly.

Create a build directory to keep the compiled libraries and make it the current working directory:

$ mkdir build
$ cd build

Now, run CMake for creating the build scripts:

$ cmake ..

If this command fails because CMake cannot find FILIB, add the FILIB_ROOT environment variable with the path to the FILIB source code directory used during the installation.

$ FILIB_ROOT=<FILIB-directory> cmake ..

Finally, build all targets by invoking the CMake build command:

$ cmake --build .

Using the Library

The Kodiak library is used in your own C/C++ programs. A good way to start is to take one of the existing .cpp files in the examples directory and adapt it to your purposes. You can either invoke the compiler directly with a link to the filib++ and Kodiak libraries, or else add a new entry to the examples/CMakeLists.txt file. For C programs, please use the src/Adapters/Codiak.h header file to invoke Kodiak's routines.

Be aware that care must be taken with the order in which commands are invoked. All variables should be declared before any variable resolutions are set.

Version

Kodiak ver. 2.0.4, July 2022

Logo

The Kodiak logo was designed by Mahyar Malekpour (NASA).

License and Copyright Notice

The code in this repository is released under NASA's Open Source Agreement. See the directory LICENSES.

Notices:

Copyright 2017 United States Government as represented by the
   Administrator of the National Aeronautics and Space Administration.
   All Rights Reserved.

Disclaimers:

No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY
WARRANTY OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY,
INCLUDING, BUT NOT LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE
WILL CONFORM TO SPECIFICATIONS, ANY IMPLIED WARRANTIES OF
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, OR FREEDOM FROM
INFRINGEMENT, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL BE ERROR
FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF PROVIDED, WILL CONFORM TO
THE SUBJECT SOFTWARE.  THIS AGREEMENT DOES NOT, IN ANY MANNER,
CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR RECIPIENT
OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR ANY
OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE.
FURTHER, GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES
REGARDING THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE,
AND DISTRIBUTES IT "AS IS."

Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS
AGAINST THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND
SUBCONTRACTORS, AS WELL AS ANY PRIOR RECIPIENT.  IF RECIPIENT'S USE OF
THE SUBJECT SOFTWARE RESULTS IN ANY LIABILITIES, DEMANDS, DAMAGES,
EXPENSES OR LOSSES ARISING FROM SUCH USE, INCLUDING ANY DAMAGES FROM
PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S USE OF THE SUBJECT
SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE UNITED
STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY
PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW.  RECIPIENT'S SOLE
REMEDY FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL
TERMINATION OF THIS AGREEMENT.

More Repositories

1

openmct

A web based mission control framework.
JavaScript
11,117
star
2

fprime

FΒ΄ - A flight software and embedded systems framework
C++
9,868
star
3

NASA-3D-Resources

Here you'll find a growing collection of 3D models, textures, and images from inside NASA.
Mathematica
2,804
star
4

astrobee

NASA Astrobee Robot Software
C++
811
star
5

apod-api

Astronomy Picture of the Day API service
Python
779
star
6

earthdata-search

Earthdata Search is a web application developed by NASA EOSDIS to enable data discovery, search, comparison, visualization, and access across EOSDIS' Earth Science data holdings.
JavaScript
728
star
7

trick

Trick Simulation Environment. Trick provides a common set of simulation capabilities and utilities to build simulations automatically.
C++
685
star
8

Transform-to-Open-Science

Transformation to Open Science
639
star
9

cFS

The Core Flight System (cFS)
CMake
537
star
10

XPlaneConnect

The X-Plane Communications Toolbox is a research tool used to interact with the X-Plane flight simulator
C
536
star
11

osal

The Core Flight System (cFS) Operating System Abstraction Layer (OSAL)
C
486
star
12

api-docs

api.nasa.gov
SCSS
420
star
13

NASTRAN-95

Fortran
393
star
14

spaceapps

366
star
15

cFE

The Core Flight System (cFS) Core Flight Executive (cFE)
C
343
star
16

World-Wind-Java

World Wind, an open source 3D interactive world viewer, was created by NASA's Learning Technologies project, and released in mid-2004. It is now developed by NASA staff and open source community developers.
C++
328
star
17

instructions

https://github.com/nasa/nasa.github.io/blob/master/docs/INSTRUCTIONS.md
HTML
322
star
18

ogma

Haskell
318
star
19

Common-Metadata-Repository

Clojure
302
star
20

VICAR

291
star
21

CFL3D

Fortran
267
star
22

Open-Source-Catalog

Contains the NASA open source software catalog for automatic deployment to code.nasa.gov
JavaScript
259
star
23

code-nasa-gov

code.nasa.gov site leveraging the Open Source Catalog on github.com, powered by Polymer
CSS
236
star
24

eefs

EEPROM File System
C
232
star
25

cumulus

Cumulus Framework + Cumulus API
JavaScript
230
star
26

openmct-tutorial

A tutorial for OpenMCT that guides you through integrating historical and realtime telemetry.
JavaScript
221
star
27

T-MATS

An open source thermodynamic modeling package completed on behalf of NASA. The Toolbox for the Modeling and Analysis of Thermodynamic Systems (T-MATS) package offers a MATLAB/Simulink toolbox that gives a developer the ability to create simulations of such thermodynamic systems as turbomachinery and gas turbines. Keywords: TMATS, Control System, Numerical Methods, Newton-Raphson, Jacobian Calculation, Propulsion, Aircraft Engine, Jet, Turbofan, Turbojet, Compressor, Turbine, Nozzle, Inlet, open source
HTML
216
star
28

isle

JavaScript
213
star
29

europa

C++
207
star
30

nasa-latex-docs

An easy and convenient package to create technical LaTeX documents.
TeX
197
star
31

pvslib

NASA PVS Library of Formal Developments
Common Lisp
186
star
32

delta

Deep Learning for Satellite Imagery
Python
184
star
33

CrisisMappingToolkit

NASA Ames Crisis Mapping Toolkit
Python
183
star
34

nos3

NASA Operational Simulator for Small Satellites
C
167
star
35

icarous

ICAROUS is a software architecture for the development of UAS applications
C
147
star
36

DERT

DERT is an open source software tool for exploring NASA's digital terrain models in 3D
Java
142
star
37

NASTRAN-93

NASTRAN is the NASA Structural Analysis System, a finite element analysis program (FEA)
Fortran
134
star
38

ow_simulator

Python
129
star
39

meshNetwork

C++
127
star
40

prog_models

The NASA Prognostic Model Package is a Python framework focused on defining and building models for prognostics (computation of remaining useful life) of engineering systems, and provides a set of prognostics models for select components developed within this framework, suitable for use in prognostics applications for these components.
121
star
41

QuIP

QuIP provides an interactive environment for computing and presenting images and image sequences, manipulating and storing arbitrary data, and general scientific computing and plotting. The current release supports unix-like operating systems (tested on Linux and Mac OSX), and Apple's iOS mobile operating system. GPU acceleration is supported with either CUDA or OpenCL. There is built-in support for psychophysical experimentation, with general-purpose staircase routines and analysis of psychometric functions.
C
118
star
42

autodoc

Create Microsoft Documents automatically using Text and Template files
106
star
43

PrognosticsAlgorithmLibrary

MATLAB
103
star
44

CompDam_DGD

Fortran
99
star
45

astrobee_android

NASA Astrobee Robot Software, Android
Java
96
star
46

OpenSPIFe

The Open Scheduling and Planning Interface for Exploration (OpenSPIFe) is an integrated planning and scheduling toolkit based on hundreds of hours of expert observation, use, and refinement of state-of-the-art planning and scheduling technology for several applications within NASA.
Java
95
star
47

PrognosticsModelLibrary

MATLAB
89
star
48

mmt

NASA's Metadata Management Tool.
Ruby
86
star
49

kepler-pipeline

Kepler Science Data Processing Pipeline
C
84
star
50

IDF

C++
80
star
51

EMIT-Data-Resources

This repository provides guides, short how-tos, and tutorials to help users access and work with data from the Earth Surface Mineral Dust Source Investigation (EMIT) mission.
HTML
79
star
52

nasapress

A WordPress theme built on the NASA Web Design Standards
PHP
79
star
53

PyTDA

Python Turbulence Detection Algorithm (PyTDA)
Jupyter Notebook
78
star
54

podaacpy

A python utility library for interacting with NASA JPL's PO.DAAC
Python
74
star
55

RHEAS

Regional Hydrologic Extremes Assessment System
Python
73
star
56

astrobot

A slack bot integration with NASA data
JavaScript
73
star
57

CCDD

CFS Command and Data Dictionary Tool (CCDDT)
Java
72
star
58

SMCPy

Python module for uncertainty quantification using a parallel sequential Monte Carlo sampler
Python
71
star
59

NASA-Acronyms

JavaScript
71
star
60

PointCloudsVR

C++
68
star
61

harmony

Application for providing services for Earth observation data in the cloud using standards-based APIs
TypeScript
68
star
62

channel-emulator

C++
66
star
63

cFS-GroundSystem

The Core Flight System (cFS) Ground System Lab Tool (cFS-GroundSystem)
Python
65
star
64

CFS-101

63
star
65

AprilNav

C++
62
star
66

common-mapping-client

CMC is a starter-kit for creating web-based mapping applications
JavaScript
60
star
67

PSP

The Core Flight System (cFS) Platform Support Package (PSP)
C
60
star
68

NASAaccess

NASAaccess is R package that can generate gridded ascii tables of climate (CIMP5) and weather data (GPM, TRMM, GLDAS) needed to drive various hydrological models (e.g., SWAT, VIC, RHESSys, ..etc)
R
60
star
69

CryptoLib

Provide a software-only solution using the CCSDS Space Data Link Security Protocol - Extended Procedures (SDLS-EP) to secure communications between a spacecraft running the core Flight System (cFS) and a ground station.
C
60
star
70

GTM_DesignSim

MATLAB
59
star
71

dictionaries

A collection of NASA "dictionaries", including thesauri, taxonomies and ontologies.
HTML
58
star
72

libSPRITE

libSPRITE is a set of libraries that have been used on several past projects including flight, technology demonstration, and simulation projects. libSPRITE provides a diverse set of functions to attempt to simplify coding and reduce code errors. For example, libSPRITE defines engineering units as types (i.e., Meters or Radians instead of double or int). It includes an engineering unit aware math library. libSPRITE includes a task scheduling system that abstracts pthreads and includes a publish subscribe data system for data routing. In addition, libSPRITE includes an optional binding to the Lua scripting language for configuring the program, setting parameters, running Lua scripts within C++ tasks and even interacting with the application during runtime.
C++
57
star
73

utm-apis

The collection of APIs for NASA's UTM project in the form of OpenAPI documents.
55
star
74

cumulus-dashboard

Cumulus API Dashboard
JavaScript
55
star
75

pretrained-microscopy-models

Python
54
star
76

GFR

GFR (Glenn Flux Reconstruction) software (LEW-19709-1) has been approved for an open source release
Fortran
54
star
77

refine

C
53
star
78

hybridq

HybridQ is a highly extensible platform designed to provide a common framework to integrate multiple state-of-the-art techniques to simulate large scale quantum circuits on a variety of hardware. HybridQ provides tools to manipulate, develop, and extend noiseless and noisy circuits for different hardware architectures. HybridQ also supports large-scale high-performance computing (HPC) simulations, automatically balancing workload among different processor nodes and enabling the use of multiple backends to maximize parallel efficiency. Everything is then glued together by a simple and expressive language that allows seamless switching from one technique to another as well as from one hardware to the next, without the need to write lengthy translations, thus greatly simplifying the development of new hybrid algorithms and techniques.
Python
53
star
79

prog_algs

The Prognostic Algorithm Package is a python framework for model-based prognostics (computation of remaining useful life) of engineering systems, and provides a set of algorithms for state estimation and prediction, including uncertainty propagation. The algorithms take as inputs prognostic models (from NASA's Prognostics Model Package), and perform estimation and prediction functions. The library allows the rapid development of prognostics solutions for given models of components and systems. Different algorithms can be easily swapped to do comparative studies and evaluations of different algorithms to select the best for the application at hand.
53
star
80

NASA-Space-Weather-Media-Viewer

Space Weather and the Sun.
52
star
81

EADINLite

EADIN_Lite Network Protocol
C++
51
star
82

SingleDop

Single Doppler Retrieval Toolkit (SingleDop)
Jupyter Notebook
50
star
83

multipath-tcp-tools

C++
49
star
84

MMM-Py

Marshall MRMS Mosaic Python Toolkit
Jupyter Notebook
48
star
85

ipv6_python

Python
47
star
86

CF

The Core Flight System (cFS) CFDP application.
C
47
star
87

MLMCPy

Python
47
star
88

TTECTrA

An open source, semi-automated, control design tool for subsonic aircraft engine simulations written in the MATLAB/Simulink environment. The Tool for Turbine Engine Closed-loop Transient Analysis provides the user a preliminary estimate of the closed-loop transient performance of an engine model.
47
star
89

WellClear

Well-Clear Boundary Models for Integration of UAS in the NAS
HTML
46
star
90

CertWare

Java
46
star
91

bingo

Python
45
star
92

cmr-stac

TypeScript
44
star
93

RtRetrievalFramework

C++
43
star
94

giant

Goddard Image Analysis and Navigation Tool
Python
43
star
95

mplStyle

Matplotlib object oriented style system
Python
43
star
96

podaac_tools_and_services

A meta-repository which essentially lists code related to all tools and services software for NASA JPL's PO.DAAC
Python
43
star
97

daidalus

open source release: LAR-19282-1 Detect and Avoid Alerting Logic for Unmanned Systems (DAIDALUS) with Dynamic Well-Clear Separation Volumes).
HTML
42
star
98

TLNS3D

Fortran
41
star
99

isaac

Integrated System for Autonomous and Adaptive Caretaking
Jupyter Notebook
41
star
100

OnAIR

The On-board Artificial Intelligence Research (OnAIR) Platform is a framework that enables AI algorithms written in Python to interact with NASA's cFS. It is intended to explore research concepts in autonomous operations in a simulated environment.
Python
41
star