diff --git a/Joshua.jpg b/Joshua.jpg new file mode 100644 index 0000000..cada5f3 Binary files /dev/null and b/Joshua.jpg differ diff --git a/Jurriaan.jpg b/Jurriaan.jpg new file mode 100644 index 0000000..5fd98f5 Binary files /dev/null and b/Jurriaan.jpg differ diff --git a/ginger-cat-713.png b/ginger-cat-713.png index beaf259..c208417 100644 Binary files a/ginger-cat-713.png and b/ginger-cat-713.png differ diff --git a/ginger-cat-718.png b/ginger-cat-718.png index c8d9115..4305967 100644 Binary files a/ginger-cat-718.png and b/ginger-cat-718.png differ diff --git a/ginger-cat-746.png b/ginger-cat-746.png index 8f20451..1ca1e3c 100644 Binary files a/ginger-cat-746.png and b/ginger-cat-746.png differ diff --git a/index.html b/index.html index c726f18..6997e85 100644 --- a/index.html +++ b/index.html @@ -53,8 +53,12 @@

What we do as BaaS

-

We provide an online service for bisimulation checking. - Developers can now check behavioural equivalence with the touch of a button, increasing their productivity. +

We provide an online service for bisimulation checking. + Bisimulation is a must in the Industry 4.0 era. + Correctness and robustness of your software products are our top priority. + With BaaS, we are changing the way you do verification. + +

Developers can now check behavioural equivalence with the touch of a button, increasing their productivity. We support many types of bisimulation, including the latest up-to techniques.

You can register for a monthly subscription which allows you to check many models. @@ -68,15 +72,18 @@

What is a bisimulation?

-

Two systems are bisimilar if they match each other's moves. +

Two systems are bisimilar if they match each other's moves. In this sense, each of the systems cannot be distinguished from the other by an observer. -

A bisimulation relation is a certificate of this equivalence. +

A bisimulation relation is a certificate of this equivalence. Our service computes this certificate automatically for you. This makes our service trustworthy and secure, as it does not only return a binary output.

If your system contains a bug, our service will not be able to produce this certificate. Instead, it will return a counterexample, which can be used to resolve the bug. + +

Bisimulations are also used to minimise your state-based systems. + this enables model-checkers to prove correctness in terms of temporal logics.

@@ -109,41 +116,56 @@ Below is a table of the different features we provide. -
You getFreePremium BaaS -
Maximal number of models per month109000 -
Maximal number of states per model501000000 -
Maximal number of transitions per model1009000000 +
You getFreePremium BaaS +
Maximal number of models per month109000 +
Maximal number of states per model501000000 +
Maximal number of transitions per model1009000000 -
Features -
Standard (strong) bisimulation✓✓ -
Branching bisimulation✓ -
Bisimulation up-to transitive closure and congruence✓ -
Bisimulation up-to bisimulation✓ -
CEGAR & CEGIS API✓ -
O(m log n) algorithms✓ -
Big Data Types✓ +
Features +
Standard (strong) bisimulation✓✓ +
Branching bisimulation✓ +
Bisimulation up-to transitive closure and congruence✓ +
Bisimulation up-to bisimulation✓ +
CEGAR & CEGIS API✓ +
O(m log n) algorithms✓ +
Big Data Types✓ -
Models -
Deterministic Automata✓✓ -
Nondeterministic Automata✓ -
Weighted Automata✓✓ -
Weighted Tree Automata✓ -
Deterministic Register Automata✓ -
Quantum Software Product Line Systems✓ -
Labelled Transition Blockchain Coalgebras✓ +
Models +
Deterministic Automata✓✓ +
Nondeterministic Automata✓ +
Weighted Automata✓✓ +
Weighted Tree Automata✓ +
Deterministic Register Automata✓ +
Quantum Software Product Line Systems✓ +
Labelled Transition Blockchain Coalgebras✓
+ +

Upon request, we can provide divergence-preserving branching bisimilarity for citizens from The Netherlands and France.

+

Team

-

A CEO, some developers, some designers, etc. - All of them have a PhD in related fields, etc. - "Bisimulation evangelist." - +

We're a team of bisimulation technologists and serious entrepreneurs. + We work around the clock, to make sure your bisimulations are always ready to go. + +

+
+
+ Joshua Moerman, PhD.
+ Founder, Bisimulation Evangelist. +
+ +
+
+ Jurriaan Rot, PhD.
+ CEO, CPO, and CTO. +
+
- Copyright 2020 JM + Copyright 2020 - BaaS - Bisimulation Online
diff --git a/star.svg b/star.svg new file mode 100644 index 0000000..f95327e --- /dev/null +++ b/star.svg @@ -0,0 +1,5 @@ + + + + + diff --git a/style.css b/style.css index 169ca75..7e35393 100644 --- a/style.css +++ b/style.css @@ -1,9 +1,12 @@ body { margin: 0; color: #034; - font-family: 'Open Sans', Frutiger, "Frutiger Linotype", Univers, Calibri, "Gill Sans", "Gill Sans MT", "Myriad Pro", Myriad, "DejaVu Sans Condensed", "Liberation Sans", "Nimbus Sans L", Tahoma, Geneva, "Helvetica Neue", Helvetica, Arial, sans-serif; - font-size: 13pt; - line-height: 1.25em; + font-family: "Nunito Sans", "Avenir", "Helvetica Neue", sans-serif; + font-size: 14pt; + line-height: 1.4em; +} +p { + text-align: justify; } a { @@ -79,10 +82,9 @@ h2 { h3 { color: #dd3b2a; - font-family: 'Adelle W01 Bold', 'Arvo', Constantia, "Lucida Bright", Lucidabright, "Lucida Serif", Lucida, "DejaVu Serif", "Bitstream Vera Serif", "Liberation Serif", Georgia, serif; - font-size: 40px; - font-weight: 500; - line-height: 1em; + text-transform: uppercase; + font-size: 160%; + font-weight: 900; } .main { @@ -145,6 +147,26 @@ table td { border-bottom: 2px solid #dd3b2a; } +.team { + display: grid; + grid-template-columns: auto auto; + grid-gap: 30px; + align-items: top; +} + +.profile { + text-align: center; + max-width: 220px; + margin: 0 auto; +} + +.profile-pic { + margin: 20px; + width: 160px; + border-radius:100px; + box-shadow: 0 0 10px 0 black; +} + /* star */ @keyframes spin { from { transform: rotate(0deg); } @@ -152,8 +174,7 @@ table td { } aside:before { animation: spin 37s infinite linear; - /*background: url('../images/starburst.png') center top no-repeat;*/ - background: url('data:image/svg+xml;base64, PD94bWwgdmVyc2lvbj0iMS4wIiBlbmNvZGluZz0idXRmLTgiPz4NCjwhLS0gR2VuZXJhdG9yOiBBZG9iZSBJbGx1c3RyYXRvciAxNi4wLjQsIFNWRyBFeHBvcnQgUGx1Zy1JbiAuIFNWRyBWZXJzaW9uOiA2LjAwIEJ1aWxkIDApICAtLT4NCjwhRE9DVFlQRSBzdmcgUFVCTElDICItLy9XM0MvL0RURCBTVkcgMS4xLy9FTiIgImh0dHA6Ly93d3cudzMub3JnL0dyYXBoaWNzL1NWRy8xLjEvRFREL3N2ZzExLmR0ZCI+DQo8c3ZnIHZlcnNpb249IjEuMSIgaWQ9IkxheWVyXzEiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9yZy8yMDAwL3N2ZyIgeG1sbnM6eGxpbms9Imh0dHA6Ly93d3cudzMub3JnLzE5OTkveGxpbmsiIHg9IjBweCIgeT0iMHB4Ig0KCSB3aWR0aD0iOTIyLjU3NHB4IiBoZWlnaHQ9IjkyMS4wNzJweCIgdmlld0JveD0iMCAwIDkyMi41NzQgOTIxLjA3MiIgZW5hYmxlLWJhY2tncm91bmQ9Im5ldyAwIDAgOTIyLjU3NCA5MjEuMDcyIg0KCSB4bWw6c3BhY2U9InByZXNlcnZlIj4NCjxwb2x5Z29uIGZpbGw9IiNGRkZGRkYiIHBvaW50cz0iNzQ1Ljk0NSw4MjkuMDQyIDUxNS4wNzIsNTc3LjIyMiA1NzIuNjM1LDkxMy45NzIgNDY0LjE0Niw1OTAuMDIgMzc5Ljc2Myw5MjEuMDcyIDQxMi40MjEsNTgwLjk5OSANCgkyMDAuNjgyLDg0OS4xMDggMzY4LjgzNSw1NTEuNzIxIDY2LjM1Miw3MTAuNTI2IDM0MC45MjgsNTA3LjIzOSAwLDUyOS4yOTEgMzMzLjUyLDQ1NS4yNTYgMTMuMTAxLDMzNi43MzEgMzQ3Ljg5Niw0MDQuNzU2IA0KCTEwMy4zOTMsMTY2LjE1MyAzODEuNTc2LDM2NC40NzEgMjU1LjI1Nyw0Ny4wNDUgNDI4LjcyNCwzNDEuMzY2IDQ0Mi40MzYsMCA0ODEuMTk3LDMzOS40MzUgNjMyLjU2NiwzMy4xNTcgNTI5LjkyLDM1OS4wMTIgDQoJNzkyLjc3NiwxNDAuNzgyIDU2Ni40NjgsMzk2LjcxNCA4OTUuMzU2LDMwNC4yNjQgNTg0LjUxNCw0NDYuMDIxIDkyMi41NzQsNDk1LjMzNiA1ODAuOTUxLDQ5OC40MDkgODY5LjcyNCw2ODAuOTY0IA0KCTU1Ni4zODgsNTQ0LjgxNSAiLz4NCjwvc3ZnPg0K') center top no-repeat; + background: url('star.svg') center top no-repeat; content: ''; height: 921px; left: 50%; @@ -251,4 +272,13 @@ footer a:hover { table td { padding: 4px; } + table { + font-size: 80%; + } + .team { + grid-template-columns: auto; + } + .profile { + max-width: 400px; + } } \ No newline at end of file