From 41121f643c9c635b7cb7292d564f540ad8b39523 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Sun, 20 Mar 2016 00:05:48 0400
Subject: [PATCH] books/bookvolbib Add Sutt13, Computing the Complete CS
Decomposition
Goal: Axiom Numerics
@article{Sutt13,
author = "Sutton, Brian D.",
title = "Computing the Complete CS Decomposition",
year = "2013",
month = "February",
url = "http://arxiv.org/pdf/0707.1838v3.pdf",
paper = "Sutt13.pdf",
abstract =
"An algorithm is developed to compute the complete CS decomposition
(CSD) of a partitioned unitary matrix. Although the existence of the
CSD has been recognized since 1977, prior algorithms compute only a
reduced version (the 2by1 CSD) that is equivalent to two
simultaneous singular value decompositions. The algorithm presented
here computes the complete 2by2 CSD, which requires the simultaneous
diagonalization of all four blocks of a unitary matrix partitioned
into a 2by2 block structure. The algorithm appears to be the only
fully specified algorithm available. The computation occurs in two
phases. In the first phase, the unitary matrix is reduced to
bidiagonal block form, as described by Sutton and Edelman. In the
second phase, the blocks are simultaneously diagonalized using
techniques from bidiagonal SVD algorithms of Golub, Kahan, and
Demmel. The algorithm has a number of desirable numerical features."
}

books/bookvolbib.pamphlet  28 +++++++++++++++
changelog  2 +
patch  73 ++++++++++++
src/axiomwebsite/patches.html  2 +
4 files changed, 55 insertions(+), 50 deletions()
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 8a91fcc..2336d54 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 2071,6 +2071,34 @@ when shown in factored form.
\end{chunk}
+\index{Sutton, Brian D.}
+\begin{chunk}{axiom.bib}
+@article{Sutt13,
+ author = "Sutton, Brian D.",
+ title = "Computing the Complete CS Decomposition",
+ year = "2013",
+ month = "February",
+ url = "http://arxiv.org/pdf/0707.1838v3.pdf",
+ paper = "Sutt13.pdf",
+ abstract =
+ "An algorithm is developed to compute the complete CS decomposition
+ (CSD) of a partitioned unitary matrix. Although the existence of the
+ CSD has been recognized since 1977, prior algorithms compute only a
+ reduced version (the 2by1 CSD) that is equivalent to two
+ simultaneous singular value decompositions. The algorithm presented
+ here computes the complete 2by2 CSD, which requires the simultaneous
+ diagonalization of all four blocks of a unitary matrix partitioned
+ into a 2by2 block structure. The algorithm appears to be the only
+ fully specified algorithm available. The computation occurs in two
+ phases. In the first phase, the unitary matrix is reduced to
+ bidiagonal block form, as described by Sutton and Edelman. In the
+ second phase, the blocks are simultaneously diagonalized using
+ techniques from bidiagonal SVD algorithms of Golub, Kahan, and
+ Demmel. The algorithm has a number of desirable numerical features."
+}
+
+\end{chunk}
+
\index{Yang, Xiang}
\index{Mittal, Rajat}
\begin{chunk}{ignore}
diff git a/changelog b/changelog
index 85719c3..8e1e5b8 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20160320 tpd src/axiomwebsite/patches.html 20160320.01.tpd.patch
+20160320 tpd books/bookvolbib Sutt13, Computing the Complete CS Decomposition
20160319 tpd src/axiomwebsite/patches.html 20160319.05.tpd.patch
20160319 tpd books/bookvolbib Add Nguy16 on Higherorder symbolic execution
20160319 tpd src/axiomwebsite/patches.html 20160319.04.tpd.patch
diff git a/patch b/patch
index ff93acf..545c3ac 100644
 a/patch
+++ b/patch
@@ 1,54 +1,27 @@
books/bookvolbib Add Nguy16 on Higherorder symbolic execution
+books/bookvolbib Add Sutt13, Computing the Complete CS Decomposition
Goal: Proving Axiom Correct
+Goal: Axiom Numerics
@article{Nguy16,
 author = "Nguyen, Phuc C. and TobinHochstadt, Sam and van Horn, David",
 title = "Higherorder symbolic execution for contract verification and
 refutation",
 url = "http://arxiv.org/pdf/1507.04817v2.pdf",
 year = "2016",
+@article{Sutt13,
+ author = "Sutton, Brian D.",
+ title = "Computing the Complete CS Decomposition",
+ year = "2013",
month = "February",
 paper = "Nguy16.pdf",
 abstract =
 "We present a new approach to automated reasoning about higherorder
 programs by endowing symbolic execution with a notion of higherorder,
 symbolic values.

 To validate our approach, we use it to develop and evaluate a system
 for verifying and refuting behavioral software contracts of components
 in a functional language, which we call {\sl soft contract
 verification}. In doing so, we discover a mutually beneficial relation
 between behavioral contracts and higherorder symbolic
 execution. Contracts aid symbolic execution by providing a rich
 language of specifications that can serve as the basis of symbolic
 higherorder values; the theory of blame enables modular verification
 and leads to the theorem that {\sl verified compnents can't be
 blamed}; and the runtime monitoring of contracts enables {\sl soft}
 verification whereby verified and unverified components can safely
 interact and verification is not an allornothing
 proposition. Conversely, symbolic execution aids contracts by
 providing compiletime verification which increases assurance and
 enables optimizations; automated testcase generation for contracts
 with counterexamples; and engendering a virtuous cycle between
 verification and the gradual spread of contracts.

 Our system uses higherorder symbolic execution, leveraging contracts
 as a source of symbolic values including unknown behavioral values,
 and employs an updatable heap of contract invariants to reason about
 flowsensitive facts. Whenever a contract is refuted, it reports a
 concrete {\sl counterexample} reproducing the error, which may involve
 solving for an unknown function. The approach is able to analyze
 firstclass contracts, recursive data structures, unknown functions,
 and controlflowsensitive refinement of values, which are all
 idiomatic in dynamic languages. It makes effective use of an
 offtheshelf solver to decide problems without heavy encodings. Our
 counterexample search is sound and relatively complete with respect to
 a firstorder solver for base type values. Therefore, it can form the
 basis of automated verification and bugfinding tools for higherorder
 programs. The approach is competitive with a wide range of existing
 tools  including type systems, flow analyzers, and model checkers 
 on their own benchmarks. We have built a tool which analyzes programs
 written in Racket, and report on its effectiveness in verifying and
 refuting contracts."
+ url = "http://arxiv.org/pdf/0707.1838v3.pdf",
+ paper = "Sutt13.pdf",
+ abstract =
+ "An algorithm is developed to compute the complete CS decomposition
+ (CSD) of a partitioned unitary matrix. Although the existence of the
+ CSD has been recognized since 1977, prior algorithms compute only a
+ reduced version (the 2by1 CSD) that is equivalent to two
+ simultaneous singular value decompositions. The algorithm presented
+ here computes the complete 2by2 CSD, which requires the simultaneous
+ diagonalization of all four blocks of a unitary matrix partitioned
+ into a 2by2 block structure. The algorithm appears to be the only
+ fully specified algorithm available. The computation occurs in two
+ phases. In the first phase, the unitary matrix is reduced to
+ bidiagonal block form, as described by Sutton and Edelman. In the
+ second phase, the blocks are simultaneously diagonalized using
+ techniques from bidiagonal SVD algorithms of Golub, Kahan, and
+ Demmel. The algorithm has a number of desirable numerical features."
}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 1c0769d..c291a37 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5236,6 +5236,8 @@ books/bookvolbib fix typo
books/bookvol10.5 update BLAS to 3.6.0 with lisp code
20160319.05.tpd.patch
books/bookvolbib Add Nguy16 on Higherorder symbolic execution
+20160320.01.tpd.patch
+books/bookvolbib Sutt13, Computing the Complete CS Decomposition

1.7.5.4