CPUs making errors. The ratio of errors is known to the manufacturers, and they adapt, trying to minimize the effects of the errors by way of firmware and redundancies and whatnot.
But someone at Intel or AMD can tell you whether I've understood it wrong or not.
Now the human brain, that's a thing with an enormous tolerance for misfires. A CPU has less misfires, but less tolerance too, since it trusts itself more.
Discussion on:
View:
Show:
But the difference between good and great software is how the software handles the hardware error. Critical failure, soft failure, reset, error acceptance, and error correction are all options, but only one keeps everything running smoothly.
Are the solution (not sure if they are the kind used in NASA projects) but the Intel CISC chips wind up with too much overhead and errors, in terms of complexity in programming the stack. RISC chips' purpose is to minimize those errors in instruction execution (as far as I understand it, but I am not a programmer so 
) so wouldn't that help as well, at the processor level?
) so wouldn't that help as well, at the processor level? 
That's the tipping over point where the producer of the thingy can start thinking profit, it's got naff all to to with correct and everything to do with acceptable.
We get buggy software and iffy machines because we accept them in return for a lower cost...
We get buggy software and iffy machines because we accept them in return for a lower cost...
It's always a trade off. What confidence level are you looking at? For an internet router your confidence level is that packets go where they're supposed to and is expressed in percentage.
95% you can buy a no name router from Taiwan for $10. 99% you buy a commercial grade Linksys at Walmart for $100. 99.99% you buy a Cisco or Jupiter for $1000 or more. 99.99966% you come talk to me, and the cost is about the same as a good used car.
My point is that there is a trade off, and it follows a very predictable curve. We want 100%, but we settle with what we can afford. I consider myself an exception to this rule, as do most people I am sure. The difference is that I will not subsidise shoddy work, nor will I pay more than I can afford. This attitude has raised the bar and changed the methods. The difference is in the implementation and utilisation rather than the brand on the case... the software makes a huge impact.
95% you can buy a no name router from Taiwan for $10. 99% you buy a commercial grade Linksys at Walmart for $100. 99.99% you buy a Cisco or Jupiter for $1000 or more. 99.99966% you come talk to me, and the cost is about the same as a good used car.
My point is that there is a trade off, and it follows a very predictable curve. We want 100%, but we settle with what we can afford. I consider myself an exception to this rule, as do most people I am sure. The difference is that I will not subsidise shoddy work, nor will I pay more than I can afford. This attitude has raised the bar and changed the methods. The difference is in the implementation and utilisation rather than the brand on the case... the software makes a huge impact.
customers are preprared to accept. No just talking quality in terms of code base here, though that's a big bugbear of mine, but product quality. One you get in with a customer, particulalry with software, changing away from your stuff becomes a significant cost, and the alternative is probably just as bad but in a slightly different way.
I'm a pragmatically reined in perfectionist by nature, every bug I could fix, but I'm not allowed to drives me barking mad, every time I go near it, which is way too often for my comfort.
I'm a pragmatically reined in perfectionist by nature, every bug I could fix, but I'm not allowed to drives me barking mad, every time I go near it, which is way too often for my comfort.
"pragmatically reined-in perfectionist"
I could not think of a better way to describe myself or darn-near all my friends. Well put, Tony
I could not think of a better way to describe myself or darn-near all my friends. Well put, Tony
What drives me nuts is when people with no technical knowlege are allowed to make decisions about a technical product to the exclusion of technical staff.
Consider:
CEO/President/Big Cheese Education: MBA from Harvard Business
Accountant Education: Accounting and statistics from a community college
Sales and Marketing Education: Liberal arts/Underwater basket weaving
Software engineer Education: Master's degree in engineering from MIT
Who makes the deadlines, issues the specifications, promises things to the client, and decides the product is ready to ship? Yeah, these people actually did run a company, and I worked under the MIT grad. We quit for the reasons you described and the company tanked 3 months later.
Learning from this lesson, Everyone in my organisation is a tech. The 51 year old grandmother who runs the office is about to get her A+. Our priorities are clear, and everyone knows how to apply the brakes if something isn't right. We guarantee our product to have 99.99966% (six-sigma) scheduled uptime. and there has been no failures to date.
Bottom line: bug free secure software can be done. Make the main loop simple and flawless, then only commit modules when they are ready. Finally, ship when you have the feature set complete.
Consider:
CEO/President/Big Cheese Education: MBA from Harvard Business
Accountant Education: Accounting and statistics from a community college
Sales and Marketing Education: Liberal arts/Underwater basket weaving
Software engineer Education: Master's degree in engineering from MIT
Who makes the deadlines, issues the specifications, promises things to the client, and decides the product is ready to ship? Yeah, these people actually did run a company, and I worked under the MIT grad. We quit for the reasons you described and the company tanked 3 months later.
Learning from this lesson, Everyone in my organisation is a tech. The 51 year old grandmother who runs the office is about to get her A+. Our priorities are clear, and everyone knows how to apply the brakes if something isn't right. We guarantee our product to have 99.99966% (six-sigma) scheduled uptime. and there has been no failures to date.
Bottom line: bug free secure software can be done. Make the main loop simple and flawless, then only commit modules when they are ready. Finally, ship when you have the feature set complete.
I've worked for people who got it wrong and tanked, I've worked for people who got it right and are ridiculously succesful.
The thing is while we might have a passion for writing the best code we could they have have a passion for selling the best code they can afford us to write and make a nice juicy profit.
They aren't wong either, ready is a really fuzzy concept on occasion...
If Bill had waited for bug free windows, a lot of us would be seriously out of a job...
The thing is while we might have a passion for writing the best code we could they have have a passion for selling the best code they can afford us to write and make a nice juicy profit.
They aren't wong either, ready is a really fuzzy concept on occasion...
If Bill had waited for bug free windows, a lot of us would be seriously out of a job...
Just fewer of us and hardware centric. There would also be a stronger Unix presence, though I doubt we would see the innovation that we have in the last 15-20 years.
an explosion in the job market. To get a similar effect it would have been pretty much the same rationale. Don't think it would affected me as I predate both techs, but without someone like Ms and intel, I'd still be fixing minor coding errors by poking an extra hole in a piece of paper tape. The tipping point was when techs became more expensive than computer time, eaily solved by create more techs., sometimes real ones...
I think I love you. 
"What drives me nuts is when people with no technical knowlege are allowed to make decisions about a technical product to the exclusion of technical staff. "
Exactly.. that's what I've been saying in this thread. The business model needs to change. I told Tony before, if one company does it, others will (should) follow. Those who don't should go out of business, by way of customers not buying their shoddy products.
"What drives me nuts is when people with no technical knowlege are allowed to make decisions about a technical product to the exclusion of technical staff. "
Exactly.. that's what I've been saying in this thread. The business model needs to change. I told Tony before, if one company does it, others will (should) follow. Those who don't should go out of business, by way of customers not buying their shoddy products.
and probably hit and lock up the market, before you release.
Don't confuse technical execellence with business excellence, uinless excellence IS the product, you'll go bust, and quick.
Even worse situation in terms of mass production, imagine if some one had been dumb enough to mass market a product that would last a lifetime, in terms of mmeting the perceieved need, never mind actually. Planned obscolescence is a necessity for it to be a viable business.
Don't confuse technical execellence with business excellence, uinless excellence IS the product, you'll go bust, and quick.
Even worse situation in terms of mass production, imagine if some one had been dumb enough to mass market a product that would last a lifetime, in terms of mmeting the perceieved need, never mind actually. Planned obscolescence is a necessity for it to be a viable business.
I see your point about planned obsolescence and agree, but the race to bigger, better, and faster takes care of it for us. For example, out router is not IPv6 capable, but version 2 will be when it comes out of test early next year. It will also have many other capabilities that no one has, at least not in one 15cm x 25cm x 6cm, 12W consuming, box that mounts on a wall and is administered by a web page.
When we release this gem, we have literally 15 other projects in the wings. We won't loose market because we don't narrow it to one. We raise the bar in one market and move on.
When we release this gem, we have literally 15 other projects in the wings. We won't loose market because we don't narrow it to one. We raise the bar in one market and move on.
We don't want 6000$ laptops, even if their error ratios are 0%. Especially because it doesn't cost much to make the software resistant to the errors, and even more especially, because the error rate is already insignificant compared to the error rate of the software.
And with the software it's the same thing, often the error rate is insignificant, not causing the uptime to fall significantly.
And yes, sometimes the easiest way to find the bug is by having a million people try it out on a million different machines.
I mean, FOSS lives on that; the only projects without a major beta out seem to be dead projects.
And with the software it's the same thing, often the error rate is insignificant, not causing the uptime to fall significantly.
And yes, sometimes the easiest way to find the bug is by having a million people try it out on a million different machines.
I mean, FOSS lives on that; the only projects without a major beta out seem to be dead projects.
It is interesting. And, I sense the research team is all fired up about this project.
would be if they could "lower the gain" to have their method find rogue code, say, in apps.
An automated and fast yet effective mapper to scan for certain kinds of malicious actions in the code of these very small programs would be very interesting to a lot of people with a lot of money.
An automated and fast yet effective mapper to scan for certain kinds of malicious actions in the code of these very small programs would be very interesting to a lot of people with a lot of money.
Microsoft's new app analyzer tool? I can't remember what its called, but its some tool to scan unpatched apps, similar to Secunia's tool
If someone writes a program that does something, like a game perhaps, but really it's a keylogging, screengrabbing piece of malware with trojan capacities... how would a scanner find that? It's not being unpatched, and it hasn't been tampered with... it was written to be malicious.
I doubt MS' scanner can read through everything the app does, and produce the intent behind it, but it sounds like this verification scanner could.
I doubt MS' scanner can read through everything the app does, and produce the intent behind it, but it sounds like this verification scanner could.
It's called the Microsoft Safety Scanner. They released it last month, and now, this week they released Microsoft Standalone System Sweeper. Its better than nothing, but it uses their MSE engine which I've found to be mediocre at best.
http://www.zdnet.com/blog/security/microsoft-ships-free-malware-cleaner-that-boots-from-cd-or-usb/8712?tag=nl.e540
http://www.zdnet.com/blog/security/microsoft-ships-free-malware-cleaner-that-boots-from-cd-or-usb/8712?tag=nl.e540
to X-ray the app, and lay bare, expose, verify what it actually intends to do, in heuristic terms... spotting naughty behaviour of certain known kinds?
Interesting discussion. Looks like 2 main issues: cost, and suitability for the "real world.
Re cost: There's a (back-of-the-envelope style) discussion in the seL4 paper (http://ertos.nicta.com.au/publications/papers/Klein_EHACDEEKNSTW_09.abstract). In a nutshell, the overall cost for a repeat exercise (i.e. doing something similar again, on top of what was learnt and using the tools etc developed, which is the fair comparison) is no more than twice that of traditional approaches (industry-standard QA for software that isn't highly critical). Compared to high-assurance regimes (for safety- or security-critical systems) it's actually *cheaper*. (And I don't accept at all that open-source is cheaper, the cost is just diluted and unaccounted.)
As far as suitability for the "real world" is concerned, Tony's argument seems to come down to "it doesn't solve all the world's problems (yet), so it's no good". Funny line or thinking.
Fact is that whatever critical system you build, if it's running on a faulty OS (and it must be assumed faulty unless proven otherwise) then whatever you're trying to do on top can go wrong, as it is at the mercy of that OS. What the seL4 verification has done is taking the kernel out of the set of faulty parts. (Actually not completely yet: there are still uncomfortable limitations in seL4, which the team is quite open about, and working on removing. These include the assumption of the compiler generating correct code, the initialization code is not yet verified and a few others.) And it's for that reason that seL4 *will* be used in critical real-world applications, in the not too distant future.
Re the "nothing new" comment: no, this isn't VDM. And yes, people have tried this in the 70's, including verifying operating systems. They failed. NICTA succeeded. That's what you call progress.
And progress has happened in other areas as well, e.g. WRT requirements capture.
Does seL4 solve all problems of software dependability? Of course not. But there is no way to solve these *without* something like seL4. It's a first step, and it achieves massively more than has ever been achieved before.
Gernot
Re cost: There's a (back-of-the-envelope style) discussion in the seL4 paper (http://ertos.nicta.com.au/publications/papers/Klein_EHACDEEKNSTW_09.abstract). In a nutshell, the overall cost for a repeat exercise (i.e. doing something similar again, on top of what was learnt and using the tools etc developed, which is the fair comparison) is no more than twice that of traditional approaches (industry-standard QA for software that isn't highly critical). Compared to high-assurance regimes (for safety- or security-critical systems) it's actually *cheaper*. (And I don't accept at all that open-source is cheaper, the cost is just diluted and unaccounted.)
As far as suitability for the "real world" is concerned, Tony's argument seems to come down to "it doesn't solve all the world's problems (yet), so it's no good". Funny line or thinking.
Fact is that whatever critical system you build, if it's running on a faulty OS (and it must be assumed faulty unless proven otherwise) then whatever you're trying to do on top can go wrong, as it is at the mercy of that OS. What the seL4 verification has done is taking the kernel out of the set of faulty parts. (Actually not completely yet: there are still uncomfortable limitations in seL4, which the team is quite open about, and working on removing. These include the assumption of the compiler generating correct code, the initialization code is not yet verified and a few others.) And it's for that reason that seL4 *will* be used in critical real-world applications, in the not too distant future.
Re the "nothing new" comment: no, this isn't VDM. And yes, people have tried this in the 70's, including verifying operating systems. They failed. NICTA succeeded. That's what you call progress.
And progress has happened in other areas as well, e.g. WRT requirements capture.
Does seL4 solve all problems of software dependability? Of course not. But there is no way to solve these *without* something like seL4. It's a first step, and it achieves massively more than has ever been achieved before.
Gernot
which have existed for decades have not took off to any noticeable extent in the general software industry.
Requirements analysis is the intractactable problem in our industry. Way back when programmers were so close to the machine there was room for all sorts of mismatch between design and implementation, that is nowhere near as much the case at the levels of abstraction we generally work at now.
It is VDM in that it's math, using math is the problem. Freed from bookkeeping is not going to be able to relate it to that email softare change request he sent last week.
Ever....
Oh and Fred's software and his need to chnage are critical...
Probably not life threatening, but still critical....
Requirements analysis is the intractactable problem in our industry. Way back when programmers were so close to the machine there was room for all sorts of mismatch between design and implementation, that is nowhere near as much the case at the levels of abstraction we generally work at now.
It is VDM in that it's math, using math is the problem. Freed from bookkeeping is not going to be able to relate it to that email softare change request he sent last week.
Ever....
Oh and Fred's software and his need to chnage are critical...
Probably not life threatening, but still critical....
... it was also about as reliable as cars. But now...
http://thedailywtf.com/Articles/Enterprise-Dependency-Big-Ball-of-Yarn.aspx
http://thedailywtf.com/Articles/Enterprise-Dependency-Big-Ball-of-Yarn.aspx
Domino effects
House of cards
Object Oriented Programming
Rube Goldberg machines
Today's cars
Each of these are complex systems with interdependencies. They require that each part does its job well enough or the entire system fails. Perhaps we need to look at systems as massively parallel redundant systems rather than a series of calls, dependencies, and loops.
House of cards
Object Oriented Programming
Rube Goldberg machines
Today's cars
Each of these are complex systems with interdependencies. They require that each part does its job well enough or the entire system fails. Perhaps we need to look at systems as massively parallel redundant systems rather than a series of calls, dependencies, and loops.
is the name of the book. I can't remember the author,it was 2008. It was about the costs of insecure software.
But my argument is that there is a difference between not meeting requirements, and bugs.
Bugs is things like buffer overflows, where stuff goes into places that it shouldn't and causes havoc.
Requirements - my best remembered one is the American software for accepting dates that would accept any two digits into the day/month/year __/__/__ fields. A proper requirement would have specified that 01-31 were valid values for day, depending on values chosen for month, etc. I always check a date prompt now to see if it will accept 99/99/99.
When I am teaching about test specifications, the law is that it must not only do what it is supposed to do, but must not do what it is not supposed to.
Regards,
But my argument is that there is a difference between not meeting requirements, and bugs.
Bugs is things like buffer overflows, where stuff goes into places that it shouldn't and causes havoc.
Requirements - my best remembered one is the American software for accepting dates that would accept any two digits into the day/month/year __/__/__ fields. A proper requirement would have specified that 01-31 were valid values for day, depending on values chosen for month, etc. I always check a date prompt now to see if it will accept 99/99/99.
When I am teaching about test specifications, the law is that it must not only do what it is supposed to do, but must not do what it is not supposed to.
Regards,
The viewpoint of meeting requirements versus bugs is one that I have not pondered. Thank you.
I can't argue with your last statement at all.
I can't argue with your last statement at all.
Go to the business types and argue for doing it right so you can save money later when right is going to become wrong. They won't be interested, not even a little bit.
Their promotion or bonus, or fiscal report or share price is based on getting something that can be sold as acceptable out by the end of next week, next month some other fool can deal with the fallout.
Usually the geek who was arguing against the short term give me mine now approach, if they don't get blamed and sacked for it.
Their promotion or bonus, or fiscal report or share price is based on getting something that can be sold as acceptable out by the end of next week, next month some other fool can deal with the fallout.
Usually the geek who was arguing against the short term give me mine now approach, if they don't get blamed and sacked for it.
Hi Michael-factoring in the human has always been a part of software functions. Code is built, designs are analysed and the software is used mainly by humans. So as I see it the main problem to software stability is the human. And until such things as security software and OS software can be built without human intervention there will always be bugs. Logical Computer Software ? able to think on its own and make the corrections. Possible ?
As soon as we have defined a machine that is as powerful as a Turing machine to be complete enough and solve problems based on algorithms using those capabilities, the system becomes complex enough that the problem it is spposed to solve becomes provably correct. If it was, the system would be incomplete and limited to a few ranges of problems and solutions, or it won't find any solution in a finite time over a finite machine. It is even sometimes impossible to predict that the result will be incorrect. (there's a mathematical proof of this...)
One common example: it is most often impossible to determine if the program will terminate, if it contains loops with conditional breaks, because it is alsmost impossible to determine tha this condition will be satisfied, except in very few cases (such as counted loops where the loop counter is warrantied of strictly *never* being modified outside of the surrounding loop control : this is a frequent case in almost all softwares, but that does not cover many other cases, less frequent, but still present in almost all softwares).
So to solve this issue, one has to find a definition of what is considered a "correct" result, in order to reduce the search space in a model with lower complexity, hiding details that are unsolvable. In many softwares, the solution exposed in its implementation is not based on a proof, impossible to assert, but on an heuristic that produces an approximatively correct solution in a finite time (independantly of its optimisation). So instead of prooving that the result you get is correct, you can just proove that the software correctly implements the heuristic (but frequently without even knowing the level of accuracy, except for some subclasses of the problems this heuristic can solve, that are far below expectations).
So what can a program verifier do ? Basically, it will try to look for uncertainties, missing assertions in the problem description or in its environment. And the software could implement, in places where it is impossible to determine that it will terminate its computation, some "watchdog" that will limit the computations to some "reasonnable" counts of passes through the atomic check, in order to decide to abort the process prematurely in order to return "no solution in a reasonnable time, the problem is too generic to be currently solvable with enough accuracy without a better heuristic implementation".
The art of programming is not really in implementing algorithms, but really into designing the heuristics, and proving that it can solve a useful subset of the exposed problems: with a better heuristic, you may be able to solve more problems, but not the full set of problems initially expected: in other words, you simplify the problem, i.e. you modify it ! The good question is if a solution found with this heuristic is also a correct solution for the unmodified problem... And here again, this last question is not solvable in a reasonable time, for the generic case !
Of course, mathematics can help, but mathematics have already proven the existence of apparently "simple" problems that have unknown number of solutions... (We call these problems "conjectures", because it is also impossible to define them as axiomes without being sure that the augmented reasonment model is provably not self-contradicting ; as long as we won't have found a demonstration, the problem will remain unknown, but there are also mathematical proofs that it is both impossible to find a demonstration of the conjecture, and a proof that it is not self-contradictory so that the system augmented with the axiome becomes completely empty).
Some examples : look for "NP-complete" problems... (does this algorithm terminate and finds the solution or prooves that it has no solution in a polynomial time, instead of a ??? much worse ??? combinatorial time ?).
But we can sometimes proove that some problems are equivalent to some already wellknown NP-complete problems (about 18 of them have been found, possibly a few more now, and their formulation is desesperately simple compared to the heavy implications about their solvability).
One common example: it is most often impossible to determine if the program will terminate, if it contains loops with conditional breaks, because it is alsmost impossible to determine tha this condition will be satisfied, except in very few cases (such as counted loops where the loop counter is warrantied of strictly *never* being modified outside of the surrounding loop control : this is a frequent case in almost all softwares, but that does not cover many other cases, less frequent, but still present in almost all softwares).
So to solve this issue, one has to find a definition of what is considered a "correct" result, in order to reduce the search space in a model with lower complexity, hiding details that are unsolvable. In many softwares, the solution exposed in its implementation is not based on a proof, impossible to assert, but on an heuristic that produces an approximatively correct solution in a finite time (independantly of its optimisation). So instead of prooving that the result you get is correct, you can just proove that the software correctly implements the heuristic (but frequently without even knowing the level of accuracy, except for some subclasses of the problems this heuristic can solve, that are far below expectations).
So what can a program verifier do ? Basically, it will try to look for uncertainties, missing assertions in the problem description or in its environment. And the software could implement, in places where it is impossible to determine that it will terminate its computation, some "watchdog" that will limit the computations to some "reasonnable" counts of passes through the atomic check, in order to decide to abort the process prematurely in order to return "no solution in a reasonnable time, the problem is too generic to be currently solvable with enough accuracy without a better heuristic implementation".
The art of programming is not really in implementing algorithms, but really into designing the heuristics, and proving that it can solve a useful subset of the exposed problems: with a better heuristic, you may be able to solve more problems, but not the full set of problems initially expected: in other words, you simplify the problem, i.e. you modify it ! The good question is if a solution found with this heuristic is also a correct solution for the unmodified problem... And here again, this last question is not solvable in a reasonable time, for the generic case !
Of course, mathematics can help, but mathematics have already proven the existence of apparently "simple" problems that have unknown number of solutions... (We call these problems "conjectures", because it is also impossible to define them as axiomes without being sure that the augmented reasonment model is provably not self-contradicting ; as long as we won't have found a demonstration, the problem will remain unknown, but there are also mathematical proofs that it is both impossible to find a demonstration of the conjecture, and a proof that it is not self-contradictory so that the system augmented with the axiome becomes completely empty).
Some examples : look for "NP-complete" problems... (does this algorithm terminate and finds the solution or prooves that it has no solution in a polynomial time, instead of a ??? much worse ??? combinatorial time ?).
But we can sometimes proove that some problems are equivalent to some already wellknown NP-complete problems (about 18 of them have been found, possibly a few more now, and their formulation is desesperately simple compared to the heavy implications about their solvability).
Basically using mathematics to see the problems of a computer program is like trying to use an x-ray machine to see the solution of a crossword puzzle.
Or like trying to cut butter with an arc, I'd imagine.
Or like trying to cut butter with an arc, I'd imagine.
Could you please explain why feel that way? Not an expert, but I was under the impression that programming and math worked together in a symbiotic relationship.
it often disproves the viability of often very promising venues of thought.
For example, a lot of linguists have been caught up in Chomsky's generative ideas about language, that the surface expressions (infinite in number) are generated on the basis of innate rules (finite in number)... but game theory supposedly has very rude things to say about that.
I don't know if the OP of this subthread is correct, but it seems to say that maths is seeing itself not applying to the case at hand. Which is funny, at least to me.
Regardless of whether it's true.
For example, a lot of linguists have been caught up in Chomsky's generative ideas about language, that the surface expressions (infinite in number) are generated on the basis of innate rules (finite in number)... but game theory supposedly has very rude things to say about that.
I don't know if the OP of this subthread is correct, but it seems to say that maths is seeing itself not applying to the case at hand. Which is funny, at least to me.
Regardless of whether it's true.
I struggled with Geodel. Thanks for reminding me. Should revisit.
B: Indeed - it is a demonstrative
A: No, that is a pronoun
B: No, it really is a demonstrative
...
That's how wars begin.
A: No, that is a pronoun
B: No, it really is a demonstrative
...
That's how wars begin.
1. The undecidability of most interesting properties of programs in Turing-complete languages is due to the fact that we cannot build a universal decider for said properties. The project discussed in the original post concerns a single program. This is crucial. We can (and did) prove a lot of interesting facts about individual programs without contradicting Goedel's incompleteness result.
2. Referring to NP-completeness is bound to mislead the uninitiated. Checking the correctness proofs is in P (ie the checker runs in time polynomial in the size of the proofs presented); creating the proofs is not known to be in NP (importantly: in the size of the claim to be proved).
Disclaimer: I'm involved in the seL4 verification project.
2. Referring to NP-completeness is bound to mislead the uninitiated. Checking the correctness proofs is in P (ie the checker runs in time polynomial in the size of the proofs presented); creating the proofs is not known to be in NP (importantly: in the size of the claim to be proved).
Disclaimer: I'm involved in the seL4 verification project.
The entire think missed me vertically by an astronomical unit.
I mean we are talking world wide blank look here....
And my boss wants to know what this enpy thing is about, he can't find any mention of it in the spec.
I mean we are talking world wide blank look here....
And my boss wants to know what this enpy thing is about, he can't find any mention of it in the spec.
Could you tell me if it's possible to check a program with a negative list?
Say, describe ten kinds of malicious behaviors, then check whether a program does any of these? In other words, do you think it potentially could root out rogue apps?
Say, describe ten kinds of malicious behaviors, then check whether a program does any of these? In other words, do you think it potentially could root out rogue apps?
look at programming by contract, formal specification notation "Z" (or as they say in euro-land, "Zed"), and PSP. personal software productivity from CMU. these are three "simple" paths that will improve your software quality now.
- Keyboard Shortcuts:
- Prev
- Next
- Toggle
