recentpopularlog in

MaxBarraclough : papers   27

Ryū: fast float-to-string conversion [ACM, open access]
Jeroen van der Zijp claims to have done better in FOX:

> New, faster, and often more accurate floating point to string conversion. No, this is not based on Ryu paper. New method reliably generates 16 digits, and does much better rounding.

http://www.fox-toolkit.org/ ( also http://www.fox-toolkit.org/ftp/fasthalffloatconversion.pdf )

The code seems to be at https://github.com/gogglesguy/fox/blob/77396c638c1c4e05/lib/fxprintf.cpp#L381
floatingPoint  algorithms  papers 
18 days ago by MaxBarraclough
Tokeneer - AdaCore case study
Links to full PDF. Discussion of the faults they found at around p46. Interesting 'Analysis' section at p59.

See also https://blog.adacore.com/tokeneer-fully-verified-with-spark-2014 , https://github.com/AdaCore/spark2014/tree/master/testsuite/gnatprove/tests/tokeneer

They used Z Notation for formal modelling.
formalMethods  papers  Ada  SPARK  Znotation 
7 weeks ago by MaxBarraclough
[PDF] The Power of Two Random Choices: A Survey of Techniques and Results
From https://news.ycombinator.com/item?id=22192971

> Suppose that n balls are thrown into n bins, with each ball choosing a bin independently and uniformly at random. Then the maximum load, or the largest number of balls in any bin, is approximately log(n) / log(log(n)) with high probability.
computerScience  statistics  papers 
8 weeks ago by MaxBarraclough
[PDF] Safe Dynamic Memory Management in Ada and SPARK [*proposal* paper]
Also https://www.adacore.com/papers/safe-dynamic-memory-management-in-ada-and-spark

> provably safe, automatic storage management without any asynchronous garbage collection, and without explicit deallocation by the user. Because the mechanism for these safe pointers relies on strict control of aliasing, it can be used in the SPARK subset for formal verification, including both information-flow analysis and proof-of-safety and correctness properties
Ada  SPARK  memoryManagement  papers  keepAnEyeOn 
9 weeks ago by MaxBarraclough
PAF: A portable assembly language [PDF]
FORTH based. Incidentally, describes the VCODE project:

> Vcode [Eng96] is a library that provides a low-level interface for generating native code quickly (10 executed instructions for generating one instruction) and portably. It was part of a research project and has not been released widely, but it inspired GNU Lightning, a production system
JIT  compilers  papers 
10 weeks ago by MaxBarraclough
Assessing Unikernel Security
Non-peer-reviewed whitepaper on unikernels' security. Makes a strong case against the way unikernels currently approach security, disabling standard OS features in the name of being lightweight.

From https://news.ycombinator.com/item?id=19738905
unikernels  security  papers  HackerNews  discussion 
may 2019 by MaxBarraclough
[PDF] Exporting Non-Exportable RSA Keys
Non-peer-reviewed paper on how Windows' 'non-exportable' certs are largely just obfuscation, not using anything like TPM

Tools exist to export non-exportable certs - https://stackoverflow.com/a/36158895/
papers  Windows  security  certificateManagement 
june 2018 by MaxBarraclough

Copy this bookmark:





to read