Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale sprachen/PVS/fault_tolerance/

Quellcode-Bibliothek

Datei: products/sources/formale sprachen/PVS/fault_tolerance/

zur Elbe Produktseite wechseln Beweissystem bei der NASA ^©

abs_props.prf
abs_props.pvs
bounded_ints.prf
bounded_ints.pvs
clock_minmax.prf
clock_minmax.pvs
clock_shift.prf
clock_shift.pvs
comm_integration.prf
comm_integration.pvs
comm_integration_stage.prf
comm_integration_stage.pvs
convergence_top.pvs
core_top.pvs
event_sequences.prf
event_sequences.pvs
exact_comm.prf
exact_comm.pvs
exact_comm_stage.prf
exact_comm_stage.pvs
exact_reduce.prf
exact_reduce.pvs
exact_reduce_integration.prf
exact_reduce_integration.pvs
exact_reduce_stage.prf
exact_reduce_stage.pvs
fault_assumptions_stage.prf
fault_assumptions_stage.pvs
finite_seqs.prf
finite_seqs.pvs
finite_sets_below_extra.prf
finite_sets_below_extra.pvs
floor_ceiling_ineq.prf
floor_ceiling_ineq.pvs
function_image_nonempty.prf
function_image_nonempty.pvs
inexact_comm.pvs
inexact_comm_stage.prf
inexact_comm_stage.pvs
inexact_reduce.prf
inexact_reduce.pvs
inexact_reduce_stage.prf
inexact_reduce_stage.pvs
integration_fault_model.prf
integration_fault_model.pvs
interval_clocks.prf
interval_clocks.pvs
inverse_clocks.prf
inverse_clocks.pvs
k_ordered.pvs
local.pvs
majority.prf
majority.pvs
majority_integration.prf
majority_integration.pvs
majority_properties.prf
majority_properties.pvs
majority_stage.prf
majority_stage.pvs
median_overlap.prf
median_overlap.pvs
median_stage.prf
median_stage.pvs
message.pvs
message_adt.pvs
middle_third_overlap.prf
middle_third_overlap.pvs
middle_third_pigeonhole.prf
middle_third_pigeonhole.pvs
middle_third_stage.prf
middle_third_stage.pvs
minmax_ineq.prf
minmax_ineq.pvs
node.prf
node.pvs
node_functions.pvs
node_functions_stage.prf
node_functions_stage.pvs
ordered_finite_sequences.prf
ordered_finite_sequences.pvs
ordered_message.prf
ordered_message.pvs
physical_clocks.prf
physical_clocks.pvs
pigeonhole.prf
pigeonhole.pvs
pigeonhole_int.prf
pigeonhole_int.pvs
protocol.prf
protocol.pvs
protocol_integration.pvs
real_finite_sequences.prf
real_finite_sequences.pvs
reduce_choice.prf
reduce_choice.pvs
reduce_properties.prf
reduce_properties.pvs
reduce_synch.prf
reduce_synch.pvs
reduce_synch_stage.prf
reduce_synch_stage.pvs
relations_extra.prf
relations_extra.pvs
select_minmax.prf
select_minmax.pvs
synch_constant_definitions.prf
synch_constant_definitions.pvs
synch_parameter_constraints.pvs
synch_protocol_invariants.prf
synch_protocol_invariants.pvs
tau_declaration.prf
tau_declaration.pvs
timing_imprecision.prf
timing_imprecision.pvs
timing_integration.prf
timing_integration.pvs
timing_integration_stage.prf
timing_integration_stage.pvs
timing_window.prf
timing_window.pvs
top.pvs
virtual_clock_1.prf
virtual_clock_1.pvs
virtual_clock_2.prf
virtual_clock_2.pvs
virtual_clock_top.pvs
virtual_clocks.prf
virtual_clocks.pvs
weber_overlap.prf
weber_overlap.pvs
weber_stage.prf
weber_stage.pvs