Episode: 3081
Title: HPR3081: Why do formal verification?
Source: https://hub.hackerpublicradio.org/ccdn.php?filename=/eps/hpr3081/hpr3081.mp3
Transcribed: 2025-10-24 16:21:25

---

This is Hacker Public Radio episode 3,081 for Monday 25 May 2020. Today's show is entitled
Why the Formal Verification. Quote,
it is hosted by Tuku Toro to
and is about 19 minutes long
and carries a clean flag. The summer is
two tour two talks about testing and formal verification of software.
This episode of HPR is brought to you by an honesthost.com.
Get 15% discount on all shared hosting
with the offer code HPR15. That's HPR15.
Better web hosting that's honest and fair at an honesthost.com.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
each and every of those generated tests it will verify that the properties that you
defined are true they hold and if not it will report that hey this specific case
failed some tools even try to minimize the test case so as soon as they
encounter a failing test they try to make it smaller like if it's a 1 million
element listed try to withdraw the list and see if it still fails they try to
find a simple example that fails as possible other tools have databases that
keep track of all the failed tests over time so when you start a new
test run they will execute those failed tests first to see that they
haven't been recursion and those have been executed they will start generating
more this data but again this will this will cover bigger amount of inputs but
this cannot cover in all cases this cannot cover all the inputs if you have two
boolands for example then and you're doing some operation with them you have
four combinations that doesn't you can actually specify by hand but if you have
a some amount of boolands and you are doing some operation to them and the
amount of combination is reasonable small this can cover all the all the
combinations but if in case you are doing something with numbers like some
big numbers then this cannot cover all the possible combinations but this can
cover much much larger area of the inputs but then if you have a some some some
really critical software that or you have some contractual application that you
have to be really really super sure that there's no problems you can try
calling with the formal proofs and this is this is the thing that I talk talk about
in that episode three thousand fifty seven formal verification look here you
treat the code as a mathematical function because if you look them from the
certain angle they are they are identical like code and mathematics are different
times of the same coin basically and then you can prove mathematically that
these properties that somebody wants your list are joining function to have
actually hold you can I didn't do this by hand but I won't think if I had to
do this I would start with both list at a zero length and prove that you get
the resultant list is a zero length list and then if you first one is a
zero length and second one is n plus one items and I would be using induction
again prove that and then the first one is n plus one items and the second one
is zero items and the last usually the most cool tricky to prove is that both
are n plus one items and then prove it that it any any arbitrary number here
the reason why we will be doing this is because we will be using the induction
mathematical induction because if we can prove that the function works as we want
with a zero and n plus one then we can say that it works with everything because
n plus one is one or two or three or four or whatever so you could you could
prove that no matter no matter how long this we give to this function it will
the resulting resulting list will be length will be the sum of those two list and
they will be all items present in correct order but so why aren't we doing this
the thing is that this is suitable only for certain languages the functions
that you are proving they there has to be a real mathematical functions so
data in data out and no no no touching hard drive no sending messages to
other systems matter so data in data out they can go out of functions but those
other functions have to obey the same rules data in data out so it really has to
be a mathematical view on the software and that's not that's not actually that's
not actually that difficult it's just because it's different than what people are
usually used to it takes a bit of time to change your change your brain to look
cold a little bit differently and learn different ways of abstracting and
combining and and splitting the software and all that stuff that every software
developer does every day but the biggest one is probably because the
proving is really tricky it takes lots of time and effort until you're really
cool at that and if redoing test is frustrating when you change the software
imagine how frustrating it must be redoing the rules because tests usually
look the full function outside they have an interface and they give data into
that and they get data out of that and then they can verify that this data that
we gave in and this output that we got out that they are what we want it to be
so it's a bit easier but when you're proving mathematically that the code
does it does what it should be you are looking inside of the function you are
looking how it has been implemented and if that implementation changes very
drastically then you prove isn't valid anymore and you have to redo it and then
of course the usual thing tests of mathematical proofs don't
currently correctness so you can have all the tests you want you can have all
the proofs that you want but your software still isn't correct this is because
the original stack could be wrong I mean the original specification could be
wrong whoever wrote it made a mistake or they could have omitted something
completely obvious to themselves that is not obvious to the developers who are
going to write it or they develop a who is reading the specification
mislanders do it or somebody could have made a mistake while writing a test or at
herend that they're proving like for example somebody could write that I want
to have a function that combines two lists together and they focus to
focus to mention that by the way in this business field that we are working on
every time you are combining lists we are putting a comma in between for whatever
for other reason but because this is not written in the specification then the developer
doesn't know that and then they cannot implement it correctly or it could be that
the person who write that I want to combine these two lists I wanted that the
resulting list only has the each item one so if you have a list one two three and another
list two three four you the resulting list will be one two three four so the duplicate
should be dropped and for the for them it might be completely obvious for example if they are
making a list of cars that are in the storehouse of course the one car is the only one
because they only have a one car you can you don't have a same car twice in the bookkeeping
so for them for them that is completely obvious but for the developer that probably isn't
completely obvious but if they if they had they had been saying that we want to instead of
least we want to use that because then the developer might understand hey set that's always
only unique items so it's not it's not that easy so as a summary so there's a cost versus gain
here like some things are best tested by humans some things are best tested by the
automated examples already verified rather so you have to do this do this and this happens
that kind of things some but you you can only cover some specific cases in that way you cannot
cover all the cases if you want to a bit more product verification you use property
property based testing or rather different kind of verification you use property based testing
because then the computer generates your test data and you verify that your system can handle
that test data be it bullets or be it but whatever use list or account in books of some company
computer can generate you that data and then use that verify that your software looks correctly
or you can go all out and mathematically prove that your software does what it is supposed to do
but then you have to use the specific languages and the cost will be much higher because it will
be much slower but in this case you can cover all the inputs hopefully that clarifies why why on
will you want to or why you wouldn't want to do formal verification with cook or some other
other tool if you have any questions comments or feedback I'm always interested in them you
can reach me by email or at the 31st they are to turn at master don't master don't thought social
keep on hacking
you've been listening to Hacker Public Radio at Hacker Public Radio dot org
we are a community podcast network that releases shows every weekday Monday through Friday
today's show like all our shows was contributed by an hbr listener like yourself if you ever
thought of recording a podcast then click on our contributing to find out how easy it really is
Hacker Public Radio was founded by the digital dog pound and the infonomican computer club
and is part of the binary revolution at binrev.com if you have comments on today's show
please email the host directly leave a comment on the website or record a follow up episode yourself
on this otherwise status today's show is released on the creative comments attribution share
free dot org lives