checking   819

« earlier    

Interview with Donald Knuth | Interview with Donald Knuth | InformIT
Andrew Binstock and Donald Knuth converse on the success of open source, the problem with multicore architecture, the disappointing lack of interest in literate programming, the menace of reusable code, and that urban legend about winning a programming contest with a single compilation.
nibble  interview  giants  expert-experience  programming  cs  software  contrarianism  carmack  oss  prediction  trends  linux  concurrency  desktop  comparison  checking  debugging  stories  engineering  hmm  idk  algorithms  books  debate  flux-stasis  duplication  parsimony  best-practices  writing  documentation  latex  intricacy  structure  hardware  caching  workflow  editors  composition-decomposition  coupling-cohesion  exposition  technical-writing  thinking 
3 days ago by nhaliday
Frama-C is organized with a plug-in architecture (comparable to that of the Gimp or Eclipse). A common kernel centralizes information and conducts the analysis. Plug-ins interact with each other through interfaces defined by the kernel. This makes for robustness in the development of Frama-C while allowing a wide functionality spectrum.


Three heavyweight plug-ins that are used by the other plug-ins:

- Eva (Evolved Value analysis)
This plug-in computes variation domains for variables. It is quite automatic, although the user may guide the analysis in places. It handles a wide spectrum of C constructs. This plug-in uses abstract interpretation techniques.
- Jessie and Wp, two deductive verification plug-ins
These plug-ins are based on weakest precondition computation techniques. They allow to prove that C functions satisfy their specification as expressed in ACSL. These proofs are modular: the specifications of the called functions are used to establish the proof without looking at their code.

For browsing unfamiliar code:
- Impact analysis
This plug-in highlights the locations in the source code that are impacted by a modification.
- Scope & Data-flow browsing
This plug-in allows the user to navigate the dataflow of the program, from definition to use or from use to definition.
- Variable occurrence browsing
Also provided as a simple example for new plug-in development, this plug-in allows the user to reach the statements where a given variable is used.
- Metrics calculation
This plug-in allows the user to compute various metrics from the source code.

For code transformation:
- Semantic constant folding
This plug-in makes use of the results of the evolved value analysis plug-in to replace, in the source code, the constant expressions by their values. Because it relies on EVA, it is able to do more of these simplifications than a syntactic analysis would.
- Slicing
This plug-in slices the code according to a user-provided criterion: it creates a copy of the program, but keeps only those parts which are necessary with respect to the given criterion.
- Spare code: remove "spare code", code that does not contribute to the final results of the program.
- E-ACSL: translate annotations into C code for runtime assertion checking.
For verifying functional specifications:

- Aoraï: verify specifications expressed as LTL (Linear Temporal Logic) formulas
Other functionalities documented together with the EVA plug-in can be considered as verifying low-level functional specifications (inputs, outputs, dependencies,…)
For test-case generation:

- PathCrawler automatically finds test-case inputs to ensure coverage of a C function. It can be used for structural unit testing, as a complement to static analysis or to study the feasible execution paths of the function.
For concurrent programs:

- Mthread
This plug-in automatically analyzes concurrent C programs, using the EVA plug-in, taking into account all possible thread interactions. At the end of its execution, the concurrent behavior of each thread is over-approximated, resulting in precise information about shared variables, which mutex protects a part of the code, etc.
Front-end for other languages

- Frama-Clang
This plug-in provides a C++ front-end to Frama-C, based on the clang compiler. It transforms C++ code into a Frama-C AST, which can then be analyzed by the plug-ins above. Note however that it is very experimental and only supports a subset of C++11
tools  devtools  formal-methods  programming  software  c(pp)  systems  memory-management  ocaml-sml  debugging  checking  rigor  oss  code-dive  graphs  state  metrics  llvm  gallic  cool  worrydream  impact  flux-stasis 
20 days ago by nhaliday
One week of bugs
If I had to guess, I'd say I probably work around hundreds of bugs in an average week, and thousands in a bad week. It's not unusual for me to run into a hundred new bugs in a single week. But I often get skepticism when I mention that I run into multiple new (to me) bugs per day, and that this is inevitable if we don't change how we write tests. Well, here's a log of one week of bugs, limited to bugs that were new to me that week. After a brief description of the bugs, I'll talk about what we can do to improve the situation. The obvious answer to spend more effort on testing, but everyone already knows we should do that and no one does it. That doesn't mean it's hopeless, though.


Here's where I'm supposed to write an appeal to take testing more seriously and put real effort into it. But we all know that's not going to work. It would take 90k LOC of tests to get Julia to be as well tested as a poorly tested prototype (falsely assuming linear complexity in size). That's two person-years of work, not even including time to debug and fix bugs (which probably brings it closer to four of five years). Who's going to do that? No one. Writing tests is like writing documentation. Everyone already knows you should do it. Telling people they should do it adds zero information1.

Given that people aren't going to put any effort into testing, what's the best way to do it?

Property-based testing. Generative testing. Random testing. Concolic Testing (which was done long before the term was coined). Static analysis. Fuzzing. Statistical bug finding. There are lots of options. Some of them are actually the same thing because the terminology we use is inconsistent and buggy. I'm going to arbitrarily pick one to talk about, but they're all worth looking into.


There are a lot of great resources out there, but if you're just getting started, I found this description of types of fuzzers to be one of those most helpful (and simplest) things I've read.

John Regehr has a udacity course on software testing. I haven't worked through it yet (Pablo Torres just pointed to it), but given the quality of Dr. Regehr's writing, I expect the course to be good.

For more on my perspective on testing, there's this.
techtariat  dan-luu  tech  software  error  list  debugging  linux  github  robust  checking  oss  troll  lol  aphorism  webapp  email  google  facebook  games  julia  pls  compilers  communication  mooc  browser  rust  programming  engineering  random  jargon  formal-methods  expert-experience  prof  c(pp)  course 
22 days ago by nhaliday
Clean Coder Blog
The discipline of cross checking instruments is baked into the marrow of every instrument pilot. Instrument pilots are taught to always interpret their instruments by cross checking them against others. After all, any single instrument can silently fail.
mcas  careless  carelessness  software  intent  ill  safety  737  boeing  programming  discipline  cross  checking  pilot  if  not  why 
29 days ago by bekishore
Continuous Code Quality | SonarSource
they have cyclomatic complexity rule
$150/year for dev edition (needed for C++ but not Java/Python)
devtools  software  ruby  saas  programming  python  formal-methods  checking  c(pp)  jvm  structure  intricacy  graphs  golang  scala  metrics  javascript 
4 weeks ago by nhaliday
AFL + QuickCheck = ?
Adventures in fuzzing. Also differences between testing culture in software and hardware.
techtariat  dan-luu  programming  engineering  checking  random  haskell  path-dependence  span-cover  heuristic  libraries  links  tools  devtools  software  hardware  culture  formal-methods  local-global  golang 
6 weeks ago by nhaliday
quality - Is the average number of bugs per loc the same for different programming languages? - Software Engineering Stack Exchange
Contrary to intuition, the number of errors per 1000 lines of does seem to be relatively constant, reguardless of the specific language involved. Steve McConnell, author of Code Complete and Software Estimation: Demystifying the Black Art goes over this area in some detail.

I don't have my copies readily to hand - they're sitting on my bookshelf at work - but a quick Google found a relevant quote:

Industry Average: "about 15 - 50 errors per 1000 lines of delivered code."
(Steve) further says this is usually representative of code that has some level of structured programming behind it, but probably includes a mix of coding techniques.

Quoted from Code Complete, found here:

If memory serves correctly, Steve goes into a thorough discussion of this, showing that the figures are constant across languages (C, C++, Java, Assembly and so on) and despite difficulties (such as defining what "line of code" means).

Most importantly he has lots of citations for his sources - he's not offering unsubstantiated opinions, but has the references to back them up.

[ed.: I think this is delivered code? So after testing, debugging, etc. I'm more interested in the metric for the moment after you've gotten something to compile.]
q-n-a  stackex  programming  engineering  nitty-gritty  error  flux-stasis  books  recommendations  software  checking  debugging  pro-rata  pls  comparison  parsimony  measure  data  objektbuch  speculation  accuracy  density 
7 weeks ago by nhaliday

« earlier    

related tags

&  2  2015  2018  2200  2202  3%  360-checking  360checking  3rd  737  a  abstraction  accessibile  accessibility  account  accountability  accounts  accuracy  acmtariat  affleck  after  agda  ai  algorithms  ally-bank  ally  allybank  almost  am  america  amp  an  analysis  and  aphorism  app  applauds  applications  article  artificialintelligence  audit  automate  automated  automation  automotive  backup  balancing  bam  bank-account  bank  bankaccount  banking  banks  banksimple  basics!  being  ben  benchmarks  best-practices  best  better  bias  big-picture  boeing  book  books  bot  brazil  break  brexit  briggs  browser  bug  bus  business  by  c(pp)  c  caching  can  capital-one  capitalone  card  cards  careless  carelessness  carmack  carp  cashback  cathyoneil  cds  changing  check  checking-account  checking-accounts  checkingaccount  checkingaccounts  checklists  chuck  clamp  clojure  code-dive  coding  communication.  communication  company’s  compare  comparison  compilers  composition-decomposition  computer-vision  concerns  concurrency  console.log  contacts  context  contrarianism  cool  cost-benefit  coupling-cohesion  course  court  credit-cards  credit-unions  credit  creditcards  creditunions  criminaljustice  cross  crypto  cs  culture  currying  dan-luu  data-science  data  dataviz  dbs  debate  debitcards  debugging  deep-learning  density  dependcy  dependency  dependent  design  desktop  detail-architecture  dev  development  devtools  diagnose  digital  discipline  divorcedwomen  diy  documentation  drop  duplication  during  dynamically  ebook  editors  education  elyssa-kirkham  elyssakirkham  emacs  email  embedded  ends  engineering  ensembles  error  estimator  eu  europe  example  existing  expert-experience  exposition  facebook  fact  fakenews  family'  fariness  fee-free  feedy  fiction  fighting  finance  finances  financial  financing  find-a-better-bank  find  findabetterbank  floss  flux-stasis  flycheck  fold  for  formal-methods  formal  formalization  fraud  free  from  frontier  functional  gallic  gamedev  games  generalization  giants  github  gobankingrates  going  golang  google's  google  googlesearch  gotchas  gradient-descent  grammar  graphics  graphs  guards  guide  happen’  hardware  haskell  he's  health  heated  heuristic  history  hjd  hmm  homepage  housing  how-to  howto  humanresources  ide  idk  if  ill  impact  implement  indexability  init  instructions  intelligence  intent  interest  interesting  interface  internet  interview  into  intricacy  investigative  is  itp  jargon  javascript  jobs  journalism  jrmc  js  julia  jun18  jvm  kavanaugh  keys  lamport  landlord  language  latanya  latex  launches  lawn  legal  libraries  library  lin  linear-models  links  linters  linux  lisp  list  literacy  llvm  loans  local-global  local  lol  machine-learning  machinelearning  margera  mcas  measure  meeting  memory-management  methods  metrics  millionairemob  mobile-banking  mobile  mobilebanking  model-class  model  money-market  money  moneymarket  mooc  movies  mower  my  mypy  myself  nancy  networking  new  nibble  nitty-gritty  no  node.js  normalization  not  npm  numerics  objektbuch  ocaml-sml  of  official  oil  on  one  online-banking  online-checking  online  onlinebank  onlinebanking  onlinechecking  opensource  openssl  optimization  orchestra  org:bleg  oss  out  pabloortellado  paper  parsimony  partial  parts  passphrase  password  path-dependence  pattern-matching  paxos  pdf  pelosi  personalitytests  php  pico  pilot  pip  plots  pls  politics  poulan  prediction  presentation  pro-rata  prof  program  programming  progress  prolog  promises  proof  protocol  proving  pump  pyflakes  python  q-n-a  raise  random  rate  recaptcha  recommendations  reference  referendum  regularization  rehab  rehab:  relay  research  resource  rigor  robinhood's  robinhood  robinhood’s  robust  rooted  roots  ruby  rubygems  runs  runtime  rust  ryte:  s18  saas  safety  saving  savings  says  scala  scanner  schumer  sci-comp  scope  search  security  seo  serial  service  sexist  shares  simple  sipc  site’s  slides  smt  software  span-cover  speculation  speed  spelling  spin  ssh  ssl  st  stackex  stackoverflow  starts  state  static  stats  stories  straton  strength  strict  string  structure  substring  syntax  synthesis  systematic-ad-hoc  systems  teaching  tech  technical-writing  technology  techtariat  tenant  terminal  test  tests  the  theorem  thinking  third  thorough  time  tla+  tla  tls  to  too-good-to-be-true  tool  tools  top-n  trained  transfer  transferring  transfers  trends  troll  trouble  trumark-financial-credit-union  trumark  trumarkfinancialcreditunion  trump  tutorial  type  types  typescript  typing  unheard-of  union  unsupervised  v3  validation  verification  via-diigo  via-ifttt  video  volt  vscode  vulnerability  watch  web-tool  web  webapp  webdesign  webdev  website  whatsapp  while  why  with  workflow  worrydream  writing  yak-shaving  yoast  your  zipcode  ‘i  ‘with   

Copy this bookmark: