diff --git a/examples/simple.rs b/examples/simple.rs
new file mode 100644
index 0000000000000000000000000000000000000000..187239d817fa0cd807821800551af8efa0dfab16
--- /dev/null
+++ b/examples/simple.rs
@@ -0,0 +1,86 @@
+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+//#[macro_use]
+extern crate klee;
+//use klee::{k_abort, k_assert, k_assume};
+
+// import the procedural macro
+use rtfm::{app, Threshold};
+
+app! {
+ // this is the path to the device crate
+ device: stm32f413,
+
+ resources: {
+ static X:u32 = 1;
+ static Y:u32 = 1;
+ },
+
+ tasks: {
+ EXTI1: {
+ path: exti1,
+ priority: 1,
+ resources: [X, Y],
+ },
+ },
+}
+
+#[inline(never)]
+fn exti1(_t: &mut Threshold, mut r: EXTI1::Resources) {
+ if *r.X > 10 {
+ *r.Y = 5;
+ } else {
+ *r.Y = 8;
+ }
+}
+
+// The `init` function
+//
+// This function runs as an atomic section before any tasks
+// are allowed to start
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_: init::Peripherals, _: init::Resources) {}
+
+// The idle loop.
+//
+// This runs after `init` and has a priority of 0. All tasks can preempt this
+// function. This function can never return so it must contain some sort of
+// endless loop.
+#[inline(never)]
+fn idle() -> ! {
+ loop {}
+}
+
+// Assignments
+//
+// Rust strives at being a safe language.
+// - Memory safety,
+// - static checking where possible
+// - run-time checking causing `panic!` on violation
+//
+// - No undefined behavior in "safe" Rust
+// - panic! in case undef behavior (e.g., div 0)
+//
+// Compiling and analysing the code using KLEE
+//
+// What problem(s) did KLEE identify
+// ** your answer here **
+//
+// Now try to solve this by contracts
+// You should not change the code, just enable the contacts
+// The `_` should be filled with concrete values
+//
+// Can you find a type invariant that satisfies BOTH pre- and post-conditions
+// at the same time.
+//
+// If not, why is that not possible?
diff --git a/examples/simple2.rs b/examples/simple2.rs
new file mode 100644
index 0000000000000000000000000000000000000000..d4adb824eadac27f6022668ae72547e9e43701cf
--- /dev/null
+++ b/examples/simple2.rs
@@ -0,0 +1,88 @@
+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+#[macro_use]
+extern crate klee;
+use klee::{k_abort, k_assert, k_assume};
+
+// import the procedural macro
+use rtfm::{app, Threshold};
+
+app! {
+ // this is the path to the device crate
+ device: stm32f413,
+
+ resources: {
+ static X:u32 = 1;
+ static Y:u32 = 1;
+ },
+
+ tasks: {
+ EXTI1: {
+ path: exti1,
+ priority: 1,
+ resources: [X, Y],
+ },
+ },
+}
+
+#[inline(never)]
+fn exti1(_t: &mut Threshold, mut r: EXTI1::Resources) {
+ if *r.X > 10 {
+ *r.Y = 5;
+ } else {
+ if *r.X < 5 {
+ *r.Y = 8;
+ }
+ }
+}
+
+// The `init` function
+//
+// This function runs as an atomic section before any tasks
+// are allowed to start
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_: init::Peripherals, _: init::Resources) {}
+
+// The idle loop.
+//
+// This runs after `init` and has a priority of 0. All tasks can preempt this
+// function. This function can never return so it must contain some sort of
+// endless loop.
+#[inline(never)]
+fn idle() -> ! {
+ loop {}
+}
+
+// Assignments
+//
+// Rust strives at being a safe language.
+// - Memory safety,
+// - static checking where possible
+// - run-time checking causing `panic!` on violation
+//
+// - No undefined behavior in "safe" Rust
+// - panic! in case undef behavior (e.g., div 0)
+//
+// Compiling and analysing the code using KLEE
+//
+// What problem(s) did KLEE identify
+// ** your answer here **
+//
+// Now try to solve this by contracts
+// You should not change the code, just enable the contacts
+// The `_` should be filled with concrete values
+//
+// Can you find a type invariant that satisfies BOTH pre- and post-conditions
+// at the same time.
+//
+// If not, why is that not possible?
diff --git a/examples/simple3.rs b/examples/simple3.rs
new file mode 100644
index 0000000000000000000000000000000000000000..deb8a3da8083c2849f1f79ebf1ba5264b644aa4f
--- /dev/null
+++ b/examples/simple3.rs
@@ -0,0 +1,88 @@
+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+#[macro_use]
+extern crate klee;
+use klee::{k_abort, k_assert, k_assume};
+
+// import the procedural macro
+use rtfm::{app, Threshold};
+
+app! {
+ // this is the path to the device crate
+ device: stm32f413,
+
+ resources: {
+ static X:u32 = 1;
+ static Y:u32 = 1;
+ },
+
+ tasks: {
+ EXTI1: {
+ path: exti1,
+ priority: 1,
+ resources: [X, Y],
+ },
+ },
+}
+
+#[inline(never)]
+fn exti1(_t: &mut Threshold, mut r: EXTI1::Resources) {
+ if *r.X < 5 {
+ let old = *r.Y;
+ for _ in 0..*r.X {
+ *r.Y += 1;
+ }
+ k_assert!(*r.Y == *r.X + old);
+ }
+}
+
+// The `init` function
+//
+// This function runs as an atomic section before any tasks
+// are allowed to start
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_: init::Peripherals, _: init::Resources) {}
+
+// The idle loop.
+//
+// This runs after `init` and has a priority of 0. All tasks can preempt this
+// function. This function can never return so it must contain some sort of
+// endless loop.
+#[inline(never)]
+fn idle() -> ! {
+ loop {}
+}
+
+// Assignments
+//
+// Rust strives at being a safe language.
+// - Memory safety,
+// - static checking where possible
+// - run-time checking causing `panic!` on violation
+//
+// - No undefined behavior in "safe" Rust
+// - panic! in case undef behavior (e.g., div 0)
+//
+// Compiling and analysing the code using KLEE
+//
+// What problem(s) did KLEE identify
+// ** your answer here **
+//
+// Now try to solve this by contracts
+// You should not change the code, just enable the contacts
+// The `_` should be filled with concrete values
+//
+// Can you find a type invariant that satisfies BOTH pre- and post-conditions
+// at the same time.
+//
+// If not, why is that not possible?
diff --git a/examples/simple4.rs b/examples/simple4.rs
new file mode 100644
index 0000000000000000000000000000000000000000..22e1b8f3128975d675d144e1674bbb5dc2c9b5d6
--- /dev/null
+++ b/examples/simple4.rs
@@ -0,0 +1,100 @@
+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+#[macro_use]
+extern crate klee;
+use klee::{k_abort, k_assert, k_assume};
+
+// import the procedural macro
+use rtfm::{app, Resource, Threshold};
+
+app! {
+ // this is the path to the device crate
+ device: stm32f413,
+
+ resources: {
+ static X:u32 = 1;
+ static Y:u32 = 1;
+ },
+
+ tasks: {
+ EXTI1: {
+ path: exti1,
+ priority: 1,
+ resources: [X, Y],
+ },
+ EXTI2: {
+ path: exti2,
+ priority: 2,
+ resources: [X, Y],
+ },
+ },
+}
+
+#[inline(never)]
+#[allow(non_snake_case)]
+fn exti1(t: &mut Threshold, EXTI1::Resources { X, mut Y }: EXTI1::Resources) {
+ X.claim(t, |x, t1| {
+ Y.claim_mut(t1, |y, _| {
+ let old = *y;
+ if *x < 5 {
+ for _ in 0..*x {
+ *y += 1;
+ }
+ //assert!(*y == *x + old);
+ }
+ });
+ });
+}
+
+fn exti2(_: &mut Threshold, _: EXTI2::Resources) {}
+
+// The `init` function
+//
+// This function runs as an atomic section before any tasks
+// are allowed to start
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_: init::Peripherals, _: init::Resources) {}
+
+// The idle loop.
+//
+// This runs after `init` and has a priority of 0. All tasks can preempt this
+// function. This function can never return so it must contain some sort of
+// endless loop.
+#[inline(never)]
+fn idle() -> ! {
+ loop {}
+}
+
+// Assignments
+//
+// Rust strives at being a safe language.
+// - Memory safety,
+// - static checking where possible
+// - run-time checking causing `panic!` on violation
+//
+// - No undefined behavior in "safe" Rust
+// - panic! in case undef behavior (e.g., div 0)
+//
+// Compiling and analysing the code using KLEE
+//
+// What problem(s) did KLEE identify
+// ** your answer here **
+//
+// Now try to solve this by contracts
+// You should not change the code, just enable the contacts
+// The `_` should be filled with concrete values
+//
+// Can you find a type invariant that satisfies BOTH pre- and post-conditions
+// at the same time.
+//
+// If not, why is that not possible?
diff --git a/examples/simple5.rs b/examples/simple5.rs
new file mode 100644
index 0000000000000000000000000000000000000000..0e5f60e23c6808764d60a8f8a892e655a925ae7b
--- /dev/null
+++ b/examples/simple5.rs
@@ -0,0 +1,96 @@
+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+#[macro_use]
+extern crate klee;
+use klee::{k_abort, k_assert, k_assume};
+
+// import the procedural macro
+use rtfm::{app, Resource, Threshold};
+
+app! {
+ // this is the path to the device crate
+ device: stm32f413,
+
+ resources: {
+ static X:u32 = 1;
+ static Y:u32 = 1;
+ },
+
+ tasks: {
+ EXTI1: {
+ path: exti1,
+ priority: 1,
+ resources: [X, Y],
+ },
+ EXTI2: {
+ path: exti2,
+ priority: 2,
+ resources: [Y],
+ },
+ },
+}
+
+#[inline(never)]
+#[allow(non_snake_case)]
+fn exti1(t: &mut Threshold, EXTI1::Resources { X, mut Y }: EXTI1::Resources) {
+ Y.claim_mut(t, |y, _| {
+ if *X < 5 {
+ for _ in 0..*X {
+ *y += 1;
+ }
+ }
+ });
+}
+
+fn exti2(_: &mut Threshold, _: EXTI2::Resources) {}
+
+// The `init` function
+//
+// This function runs as an atomic section before any tasks
+// are allowed to start
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_: init::Peripherals, _: init::Resources) {}
+
+// The idle loop.
+//
+// This runs after `init` and has a priority of 0. All tasks can preempt this
+// function. This function can never return so it must contain some sort of
+// endless loop.
+#[inline(never)]
+fn idle() -> ! {
+ loop {}
+}
+
+// Assignments
+//
+// Rust strives at being a safe language.
+// - Memory safety,
+// - static checking where possible
+// - run-time checking causing `panic!` on violation
+//
+// - No undefined behavior in "safe" Rust
+// - panic! in case undef behavior (e.g., div 0)
+//
+// Compiling and analysing the code using KLEE
+//
+// What problem(s) did KLEE identify
+// ** your answer here **
+//
+// Now try to solve this by contracts
+// You should not change the code, just enable the contacts
+// The `_` should be filled with concrete values
+//
+// Can you find a type invariant that satisfies BOTH pre- and post-conditions
+// at the same time.
+//
+// If not, why is that not possible?
diff --git a/examples/simple6.rs b/examples/simple6.rs
new file mode 100644
index 0000000000000000000000000000000000000000..ec18fe9bae4dc2c343536c5f2799de5252375cdb
--- /dev/null
+++ b/examples/simple6.rs
@@ -0,0 +1,98 @@
+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+#[macro_use]
+extern crate klee;
+use klee::{k_abort, k_assert, k_assume, k_read};
+
+// import the procedural macro
+use rtfm::{app, Resource, Threshold};
+
+app! {
+ // this is the path to the device crate
+ device: stm32f413,
+
+ resources: {
+ static X:u32 = 1;
+ static Y:u32 = 1;
+ },
+
+ tasks: {
+ EXTI1: {
+ path: exti1,
+ priority: 1,
+ resources: [X, Y],
+ },
+ EXTI2: {
+ path: exti2,
+ priority: 2,
+ resources: [X],
+ },
+ },
+}
+
+#[inline(never)]
+#[allow(non_snake_case)]
+fn exti1(t: &mut Threshold, EXTI1::Resources { X, mut Y }: EXTI1::Resources) {
+ X.claim(t, |x, _| {
+ if *x > 10 {
+ *Y = 5;
+ } else {
+ if *x < 5 {
+ *Y = 8;
+ }
+ }
+ });
+}
+
+fn exti2(_: &mut Threshold, _: EXTI2::Resources) {}
+
+// The `init` function
+//
+// This function runs as an atomic section before any tasks
+// are allowed to start
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_: init::Peripherals, _: init::Resources) {}
+
+// The idle loop.
+//
+// This runs after `init` and has a priority of 0. All tasks can preempt this
+// function. This function can never return so it must contain some sort of
+// endless loop.
+#[inline(never)]
+fn idle() -> ! {
+ loop {}
+}
+
+// Assignments
+//
+// Rust strives at being a safe language.
+// - Memory safety,
+// - static checking where possible
+// - run-time checking causing `panic!` on violation
+//
+// - No undefined behavior in "safe" Rust
+// - panic! in case undef behavior (e.g., div 0)
+//
+// Compiling and analysing the code using KLEE
+//
+// What problem(s) did KLEE identify
+// ** your answer here **
+//
+// Now try to solve this by contracts
+// You should not change the code, just enable the contacts
+// The `_` should be filled with concrete values
+//
+// Can you find a type invariant that satisfies BOTH pre- and post-conditions
+// at the same time.
+//
+// If not, why is that not possible?
diff --git a/examples/simple7.rs b/examples/simple7.rs
new file mode 100644
index 0000000000000000000000000000000000000000..bb91ed95dd2bd2835517774c160925877b44f247
--- /dev/null
+++ b/examples/simple7.rs
@@ -0,0 +1,100 @@
+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+#[macro_use]
+extern crate klee;
+use klee::{k_abort, k_assert, k_assume, k_read};
+
+// import the procedural macro
+use rtfm::{app, Resource, Threshold};
+
+app! {
+ // this is the path to the device crate
+ device: stm32f413,
+
+ resources: {
+ static X:u32 = 1;
+ static Y:u32 = 1;
+ },
+
+ tasks: {
+ EXTI1: {
+ path: exti1,
+ priority: 1,
+ resources: [X, Y],
+ },
+ EXTI2: {
+ path: exti2,
+ priority: 2,
+ resources: [X, Y],
+ },
+ },
+}
+
+#[inline(never)]
+#[allow(non_snake_case)]
+fn exti1(t: &mut Threshold, EXTI1::Resources { X, mut Y }: EXTI1::Resources) {
+ X.claim(t, |x, t| {
+ Y.claim_mut(t, |y, _| {
+ if *x > 10 {
+ *y = 5;
+ } else {
+ if *x < 5 {
+ *y = 8;
+ }
+ }
+ });
+ });
+}
+
+fn exti2(_: &mut Threshold, _: EXTI2::Resources) {}
+
+// The `init` function
+//
+// This function runs as an atomic section before any tasks
+// are allowed to start
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_: init::Peripherals, _: init::Resources) {}
+
+// The idle loop.
+//
+// This runs after `init` and has a priority of 0. All tasks can preempt this
+// function. This function can never return so it must contain some sort of
+// endless loop.
+#[inline(never)]
+fn idle() -> ! {
+ loop {}
+}
+
+// Assignments
+//
+// Rust strives at being a safe language.
+// - Memory safety,
+// - static checking where possible
+// - run-time checking causing `panic!` on violation
+//
+// - No undefined behavior in "safe" Rust
+// - panic! in case undef behavior (e.g., div 0)
+//
+// Compiling and analysing the code using KLEE
+//
+// What problem(s) did KLEE identify
+// ** your answer here **
+//
+// Now try to solve this by contracts
+// You should not change the code, just enable the contacts
+// The `_` should be filled with concrete values
+//
+// Can you find a type invariant that satisfies BOTH pre- and post-conditions
+// at the same time.
+//
+// If not, why is that not possible?