text:
\section{Conclusion}
\label{sec:concl}

In this paper, we proposed a method for verifying CTL properties with
respect to a (possibly infinite-space) program.
The method takes a transition system that models the input program and
a CTL formula specifying the property to prove as inputs.
It first applies proof rules from its proof system to generate a set
of forall-exists quantified Horn constraints and well-foundedness
constraints.
Then, it applies the solving algorithms \textsc{E-HSF}\xspace to solve the
generated set of Horn constraints.
The defining feature of this approach is the separation of concerns
between the encoding and the solving of the verification problem.
Although our method is based on generic Horn constraint solving
engine, it is able to outperform state-of-art methods
specialised for CTL verification.
We also demonstrate the practical applicability of the approach by
presenting an experimental evaluation using examples from the
PostgreSQL database server, the SoftUpdates patch system, the Windows
OS kernel.

\section{Constraint generation}
\label{sec:cons-gen}

The contraint generation procedure performs a top-down, recursive
descent through the syntax tree of the given CTL formula.
At each level of recursion, the procedure takes as input a CTL
satisfaction $(p(v),\mathit{next}(v,v')) \models_{\mathit{CTL}} \varphi$, where $\varphi$
is a CTL formula and assertions $p(v)$ and
$\mathit{next}(v, v')$ describe a set of states and a transition
relation, respectively.
The constraint generation procedure applies proof rules from the proof
system presented in the previous section to recursively decompose
complex satisfactions and eventually generate forall-exists quantified
Horn constraints with well-foundedness conditions.
Before starting the actual constraint generation, the procedure
recursively rewrites the input satisfaction of a given CTL formula with arbitrary
structure into a set of satisfactions of simple CTL formulas where
each simple formula is either a basic CTL state formula or an
assertion over the background theory.
The procedure then takes each satisfaction involving simple formula,
introduces auxiliary predicates and generates a sequence of
forall-exists quantified Horn constraints and well-foundedness
constraints (when needed) over these predicates.

\paragraph*{Complexity and Correctness}
The procedure performs a single top-down descent through the syntax tree
of the given CTL formula $\varphi$.
The run time for constraints generation, and hence the size of the
generated constraints, is linear in the size of $\varphi$.
Finding a solution for the generated Horn constraints is undecidable in
general.
In practice however, our solving algorithm \textsc{E-HSF}\xspace often succeeds in
finding a solution (see Section~\ref{sec:eval}).
We formalize the correctness of the constraint generation procedure in
the following theorem.
\begin{theorem}
For a given program $\ensuremath{P}$ with $\mathit{init}(v)$ and $\mathit{next}(v, v')$ over $v$ and
a CTL formula $\varphi$ the Horn constraints generated from
$(p(v),\mathit{next}(v,v')) \models_{\mathit{CTL}} \varphi$ are satisfiable if and only
if $\ensuremath{P} \models \varphi$.
\end{theorem}
The proof can be found in~\cite{KestenTCS95}.

\paragraph*{Example}
Let us consider the program given in
Figure~\ref{fig-ctl-example-code}.
It contains the variable \emph{rho} which is assigned a non-deterministic
value at Line~2.
This assignment results in the program control to move
non-deterministically following the evaluation of the condition at
Line~4.
It is common to verify such programs with respect to various CTL
properties as the non-determinism results in different computation
paths of the program.
Now, we would like to verify the program with respect to the CTL property
$\mathit{AG(EF~(WItemsNum \geq 1))}$, i.e., from every reachable
state of the program, there exists a path to a state where
\emph{WItemsNum} has a positive integer value.
\begin{figure}[h]
  \begin{lstlisting}[language=C]
      int main () {
1:       while(1) {
2:         while(1) {
              rho = nondet();
3:           if (WItemsNum<=5) {
4:             if (rho>0) break; }
5:           WItemsNum++;
6:         }
7:         while(1) {
8:           if (!(WItemsNum>2)) break;
9:           WItemsNum--;
10:        }
11:      }
12:    }
  \end{lstlisting}
  \caption{An example program}
  \label{fig-ctl-example-code}
\end{figure}

We can make the following observations about the program.
The value of the variable \emph{WItemsNum} is not set initially.
Therefore, the property is checked for any arbitrary initial value of
\emph{WItemsNum}.
The verification problem is more interesting for the case when
\emph{WItemsNum}  has a non-positive integer value.
\begin{figure}[h]
\begin{equation*}
  \begin{array}[t]{@{}rl@{\;}l@{\;}}
    v & =& (w,pc)  \\[\jot]
    \mathit{init}(v) & = &(pc=1) \\[\jot]
    \mathit{next}(v,v') & = &(pc=\ell_1 \land \mathit{pc}'=\ell_2 \land w'=w ~\lor pc=\ell_2 \land \mathit{pc}'=\ell_3 \land w'=w ~\lor \\[\jot]
          & & pc=\ell_3 \land w \leq 5 \land \mathit{pc}'=\ell_4 \land w'=w ~\lor pc=\ell_3 \land w >5 \land \mathit{pc}'=\ell_5 \land w'=w ~\lor \\[\jot]
          & & pc=\ell_4 \land \mathit{pc}'=\ell_5 \land w'=w ~\lor pc=\ell_4 \land \mathit{pc}'=\ell_7 \land w'=w ~\lor \\[\jot]
          & &  pc=\ell_5 \land \mathit{pc}'=\ell_6 \land w'=w+1 ~\lor  pc=\ell_6 \land \mathit{pc}'=\ell_3 \land w'=w ~\lor \\[\jot]
          & & pc=\ell_7 \land \mathit{pc}'=\ell_8 \land w'=w ~\lor pc=\ell_8 \land w \leq 2 \land \mathit{pc}'=\ell_{11} \land w'=w ~\lor \\[\jot]
          & & pc=\ell_8 \land w > 2 \land \mathit{pc}'=\ell_9 \land w'=w ~\lor pc=\ell_9 \land \mathit{pc}'=\ell_{10} \land w'=w-1 ~\lor \\[\jot]
          & & pc=\ell_{10} \land \mathit{pc}'=\ell_8 \land w'=w ~\lor pc=\ell_{11} \land \mathit{pc}'=\ell_3 \land w'=w)
  \end{array}
\end{equation*}
  \caption{Transition system for the example program}
  \label{fig-TS-example}
\end{figure}
This is because depending on how the variable \emph{rho} is
instantiated at Line~2, we may get a path that will not reach a state where
\emph{WItemsNum} gets a positive integer value.
For example, if we assume \emph{WItemsNum} has the value 0 initially
and \emph{WItemsNum} is instantiated to the value 1, the program
control swings between the two internal loops by keeping the value of
\emph{WItemsNum}  the same.
This resulting path will not reach the state with \emph{WItemsNum
  $\geq$ 1}.
However, if \emph{rho} is assigned a non-positive value, no matter
what the value of \emph{rho} is initially, it will eventually reach a
value greater than 5 before exiting the first nested loop.
Such a path will eventually reach the state with \emph{WItemsNum
  $\geq$ 1} and hence the program satisfies the CTL property
$AG(EF~(WItemsNum \geq 1))$.

Our method abstracts away from the concrete syntax of a programming
language by modeling a program as a transition system.
The transition system for the program is given in Figure~\ref{fig-TS-example}.

In the tuple of variables $v$, the variable $w$ corresponds to the
program variable \emph{WItemsNum} and $pc$ is the program counter
variable.
The problem of verifying the program with respect to the given property
amounts to checking if $(\mathit{init}(v), \mathit{next}(v,v'))$ satisfies
$AG(EF(w \geq 1))$, i.e., if the satisfaction $(\mathit{init}(v), \mathit{next}(v,
v')) \models_{\mathit{CTL}} AG(EF(w \geq 1))$ holds.
Our method first generates a set of Horn constraint corresponding to
the verification problem by applying the proof system.

We start constraint generation by considering the nesting structure of
$AG(EF(w \geq 1))$.
Due to the fact that $AG(EF(w \geq 1))$ has $AG$ as the outermost operator, we apply $\textsc{RuleCtlDecompUni}\xspace$
from Figure~\ref{fig-ctl-proof-rule-decompUni} to split the original
satisfaction $(\mathit{init}(v), \mathit{next}(v, v')) \models_{\mathit{CTL}} AG(EF(w \geq 1))$ into
a reduced satisfaction $(\mathit{init}(v), \mathit{next}(v, v')) \models_{\mathit{CTL}} AG(p_1(v))$ and
a new satisfaction $(p_1(v), \mathit{next}(v, v')) \models_{\mathit{CTL}} EF(w \geq 1)$.
We need to solve for the auxiliary assertion $p_1(v)$ satisfying both of
the satisfactions.

The assertion $p_1(v)$ corresponds to a set of program states that
needs to be discovered from the initial state.
This is represented by the new satisfaction $(\mathit{init}(v), \mathit{next}(v, v'))
\models_{\mathit{CTL}} AG(p_1(v))$ which is reduced directly to a set of Horn
constraints by applying $\textsc{RuleCtlAG}\xspace$
from Figure~\ref{fig-ctl-proof-rule-AG}.
This set of Horn constraints is over an auxiliary
predicate~$\mathit{inv}_1(v)$ and given below.
\begin{equation*}
  \begin{array}[t]{@{}l@{}}
    \mathit{init}(v) \rightarrow \mathit{inv}_1(v),\\[\jot]
    \mathit{inv}_1(v) \land \mathit{next}(v, v') \rightarrow \mathit{inv}_1(v'),\\[\jot]
    \mathit{inv}_1(v) \rightarrow p_1(v).
  \end{array}
\end{equation*}

The formula $EF(w \geq 1)$, which was nested in the original formula
$AG(EF(w \geq 1))$, must also be satisfied from the set of
states represented by $p_1(v)$.
This is represented by the new satisfaction $(p_1(v), \mathit{next}(v,
v')) \models_{\mathit{CTL}} EF(w \geq 1)$.
Such new satisfactions may not lead directly to Horn constraints
generation and may require further reduction into simpler
satisfactions.
Since $EF(w \geq 1)$ has $EF$ as the outermost operator, we apply
again $\textsc{RuleCtlDecompUni}\xspace$ from
Figure~\ref{fig-ctl-proof-rule-decompUni} to split the satisfaction
$(\mathtt{p}_1(v), \mathit{next}(v, v')) \models_{\mathit{CTL}} EF(w \geq 1)$ into a reduced satisfaction
$(\mathtt{p}_1(v), \mathit{next}(v, v')) \models_{\mathit{CTL}} EF(p_2(v))$ and a new
satisfaction $(p_2(v), \mathit{next}(v, v')) \models_{\mathit{CTL}} w \geq 1$.
Here also, we need to solve for the auxiliary assertion $p_2(v)$ satisfying both of
the satisfactions.

The equivalence between the formulas $EF(p_2 (v))$ and $EU(\mathit{true}, p_2
(v))$ is used to reduce the CTL satisfaction problem $(\mathtt{p}_1(v),
\mathit{next}(v, v')) \models_{\mathit{CTL}} EF(p_2(v))$ into $(p_1(v), \mathit{next}(v,v'))
\models_{\mathit{CTL}} EU(true, p_2(v))$.
The corresponding set of Horn constraints are generated by applying
$\textsc{RuleCtlEU}\xspace$ from Figure~\ref{fig-ctl-proof-rule-EU}.
Due to the existential path quantifier in $EU(true, p_2(v))$, we
obtain clauses that contain existential quantification.
We deal with the eventuality by imposing a well-foundedness condition.
This set of Horn constraints is over the auxiliary
assertions $\mathit{inv}_2(v)$ and $\mathit{rank}(v, v')$, and it is given below.
\begin{equation*}
  \begin{array}[t]{@{}l@{}}
    p_1(v) \rightarrow \mathit{inv}_2(v),\\[\jot]
    \mathit{inv}_2(v) \land \neg p_2(v) \rightarrow
    \exists v':  \mathit{next}(v, v') \land \mathit{inv}_2(v') \land \mathit{rank}(v, v'),
    \\[\jot]
    \mathit{wf}(\mathit{rank})
  \end{array}
\end{equation*}

Coming to the new satisfaction $(p_2(v), \mathit{next}(v, v')) \models_{\mathit{CTL}}
w \geq 1$, we see that its formula $w \geq 1$ is an assertion with no
temporal operators.
Since no further decomposition is possible, we apply $\textsc{RuleCtlInit}\xspace$ from
Figure~\ref{fig-ctl-proof-rule-init} to generate directly the
clause:
\begin{equation*}
    p_2(v) \rightarrow w \geq 1
\end{equation*}

As the original satisfaction $(\mathit{init}(v), \mathit{next}(v, v')) \models_{\mathit{CTL}}
AG(EF(w \geq 1))$ is reduced into the satisfactions
$(\mathit{init}(v), \mathit{next}(v, v')) \models_{\mathit{CTL}} AG(p_1(v))$,
$(p_1(v), \mathit{next}(v,v')) \models_{\mathit{CTL}} EF(p_2(v))$ and
$(p_2(v), \mathit{next}(v, v')) \models_{\mathit{CTL}} w \geq 1$,
the constraints for the original satisfaction will be the union of the
constraints for each of the decomposed satisfactions.
The Horn constraints are over the auxiliary assertions $p_1(v)$,
$\mathit{inv}_1(v)$, $p_2(v)$, $\mathit{inv}_2(v)$ and $\mathit{rank}(v, v')$, and they are
given below.
\begin{equation*}
  \begin{array}[t]{@{}l@{}}
    \mathit{init}(v) \rightarrow \mathit{inv}_1(v),\\[\jot]
    \mathit{inv}_1(v) \land \mathit{next}(v, v') \rightarrow \mathit{inv}_1(v'),\\[\jot]
    \mathit{inv}_1(v) \rightarrow p_1(v),\\[\jot]
    p_1(v) \rightarrow \mathit{inv}_2(v),\\[\jot]
    \mathit{inv}_2(v) \land \neg p_2(v) \rightarrow
    \exists v':  \mathit{next}(v, v') \land \mathit{inv}_2(v') \land \mathit{rank}(v, v'),
    \\[\jot]
    \mathit{wf}(\mathit{rank})  \\[\jot]
    p_2(v) \rightarrow w \geq 1
  \end{array}
\end{equation*}
This will be the final output of our Horn constraint generation
procedure.

\section{Evaluation}
\label{sec:eval}

We evaluate our method of CTL verification by applying the
implementation of the \textsc{E-HSF}\xspace solver on a set of industrial benchmarks
from~\cite[Figure~7]{CookPLDI13}.
These benchmarks consists of seven programs:
\texttt{Windows OS fragment 1}, \texttt{Windows OS fragment 2},
\texttt{Windows OS fragment 3}, \texttt{Windows OS fragment 4},
\texttt{Windows OS fragment 5}, \texttt{PostgreSQL pgarch} and
\texttt{Software Updates}.
For each of these programs, four slightly different versions are
considered for evaluation.
In general, the four versions of a given program are the same
in terms of the main logic of the program and what the program does,
but they may differ on the value assigned to a particular variable or
the condition for exiting a loop, etc.
This gives us a set of 28 programs.
Each such program $P$ is provided with a CTL property $\varphi$, and
there are two verification tasks associated with it: $P \models_{\mathit{CTL}}
\varphi$ and $P \models_{\mathit{CTL}} \neg\varphi$.
The existence of a proof for a property $\varphi$ for $P$ implies that $\neg\varphi$
is violated by the same program $P$, and similarly, a proof for
$\neg\varphi$ for $P$ implies that $\varphi$ is violated by $P$.
However, it may also be the case that neither $P \not\models_{\mathit{CTL}} \varphi$ nor $P \not\models_{\mathit{CTL}}
\neg\varphi$ hold.

\paragraph{Templates: }
As discussed in Section~\ref{subsec-ehsf}, \textsc{E-HSF}\xspace requires the
template functions to be provided by the user for relations with
existentially quantified variables.
For the application of CTL verification, which is the main topic of
interest in the paper, we claim that the transition relation
$\mathit{next}(v,v')$ can be used as a template by adding constraints at
each location of non-determinism.
There are two kinds of constraints that can be added depending on the
two types of possible non-determinism in $\mathit{next}(v,v')$.
\begin{itemize}
\item \textbf{non-deterministic guards: } this is the case when
  $\mathit{next}(v,v')$ has a set of more than one disjuncts with the
  same guard, i.e., there can be more than one enabled moves from a
  certain state of the program.
  For each such set, we introduce a fresh case-splitting variable and
  we strengthen the guard of each disjunct by adding a distinct
  constraint on the fresh variable.
  For example, if the set has $n$ disjuncts and $B$ is a fresh
  variable, we add the constraint $B=i$ for each disjunct $i$ where
  $1 \leq i \leq n$.
  To reason about existentially quantified queries, then it will
  suffices to instantiate $B$ to one of the values in the range
  $1\dots n$.
  Such reasoning is done by the \textsc{E-HSF}\xspace solver.
\item \textbf{non-deterministic assignments:} this is the case when
  $\mathit{next}(v,v')$ has a disjunct in which some $w'$, which is a
  subset of $v'$, is left unconstrained in the disjunct.
  In such case, we strengthen the disjunct by adding the constraint
  $x'=T_x*v+t_x $ as conjunct for each variable $x'$ in $w'$.
  Solving for $T_x$ and $t_x$ is done by the \textsc{E-HSF}\xspace solver.
\end{itemize}
In our CTL verification examples, both non-deterministic guards and
assignments are explicitly marked in the original
benchmark programs using names~$\mathtt{rho1}, \mathtt{rho2},$ etc.
We apply the techniques discussed above to generate templates from the
transition relation of each program.
In these examples, linear templates are sufficiently expressive.
For dealing with well-foundedness we use linear ranking functions.
\input{table-ehsf-eval}
We report the results in Table~\ref{table-ehsf-eval}.
For each program in Column~1, we report the shape of the property
$\varphi$ in Column~2.
The variables $p$ and $q$ in Column~2 range over the theory of
quantifier-free linear integer arithmetic.
The result as well as the time it took the \textsc{E-HSF}\xspace engine to prove the property
$\varphi$ is given in Columns~3~and~4, and similarly, the result as well
as the time it took the engine to discover a counterexample for the
negated property $\neg\varphi$ is given in Columns~5~and~6.
The symbol \checkmark\xspace marks the cases where \textsc{E-HSF}\xspace was able to find a
solution, i.e., a proof that the CTL property $\varphi$ is valid, and
the symbol $\times$~marks the cases where \textsc{E-HSF}\xspace was able to find a
counter-example, i.e., a proof that the negated CTL property
$\neg\varphi$ is not valid.
The number of LOC of each program is also given in Column~1.

The \textsc{E-HSF}\xspace engine is able to find proofs that the CTL property $\varphi$ is
valid (and the negated CTL property $\neg\varphi$ is not
valid) for all of the programs except the last three programs.
For the last three versions of \texttt{Software Updates}, not only the
negated CTL property $\neg\varphi$ but also the CTL property $\varphi$
is not valid.
This was because $\varphi$ was satisfied only for some initial states.
The method takes a total time of 52 seconds to complete the
verifications tasks.
\input{table-ehsf-comp}
Our method also compares favourably with state-of-art automated CTL
verification methods.
We present in Table~\ref{table-ehsf-comp} the comparison between the
our solving algorithm \textsc{E-HSF}\xspace and a CTL verification method from
Cook~\cite{Cook2014FTR}.
Here also, we use the programs from Table~\ref{table-ehsf-eval},
however, for the sake of focusing on the comparison, we exclude
programs for which the two methods have different outcomes.
For each program in Column~1, we report the shape of the property in
Column~2.
The time it takes \textsc{E-HSF}\xspace to prove the property $\varphi$ is given in
Column~3, and the corresponding time for Cook is given in Column~4.
Similarly, the time it takes \textsc{E-HSF}\xspace to discover a counterexample for
the negated property $\neg \varphi$ is given in
Column~5, and the corresponding time for Cook is given in Column~6.

From the result, we can see that while \textsc{E-HSF}\xspace takes a total of 48
seconds to finish the task, Cook takes a total of
149 seconds.
This amounts to an approximate reduction of 70\%.
There are a few cases where \textsc{E-HSF}\xspace takes longer than
Cook.
We suspect that a more efficient modeling of the original c program as
a transition system can help our method a lot.
The presence of many temporary program variables in the transition
relation which are not involved in any computation of the program can
affect the performance of our method.

\section{Introduction}
\label{sec-ctl-intro}

Since Pnueli's pioneering work~\cite{Pnueli1977}, the use of temporal logics has
long been recognised as a fundamental approach to the formal
specification and verification of reactive systems~\cite{Manna1992,
  Emerson1991TM}.
Temporal logics allow precise specification of complex properties.
There have been decades of effort on temporal verification of finite state
systems~\cite{Kupferman2000, Burch1990, Clarke02treelikeCEX,
  Clarke1983AVF}.
For CTL and other state-based properties, the standard procedure is to adapt
"bottom-up" (or "tableaux") techniques for reasoning on finite-state
systems.
In addition, various classes of temporal logics support
model-checking whose success over the last twenty years allows
large and complex (finite) systems to be verified automatically~\cite{Burch1990,
  Clarke1990TLM, McMillan1993SMC, Hassan2012IIC}.
In recent decades, however, the research focus has shifted to
infinite-state systems in general and to software systems in
particular as ensuring correctness for software is
in high demand.
Most algorithms for verifying CTL properties on infinite-state systems
typically involve first abstracting the state space into a finite-state
model, and then applying finite reasoning strategies on the abstract
model.
There is also a lot of effort on algorithms that are focused on a
particular fragment of CTL, such as the universal
fragment~\cite{Penczek2002BMC} and the existential
fragment~\cite{GurfinkelWC06}, or some
particular classes of infinite-state systems such as pushdown
processes \cite{Song2011, Song2013, Walukiewicz2000,
  walukiewicz2001pushdown} or parameterised
systems~\cite{Emerson1996, Demri2010checkingctl}.

In this paper, we take on the problem of automatically verifying CTL
properties for a given (possibly infinite-state) program.
We propose a method based on solving a set of forall-exists quantified
Horn constraints.
Our method takes a program $\ensuremath{P}$ modeled by a transition system
$(\mathit{init}(v), \mathit{next}(v,v'))$ and a property given by a CTL formula
$\varphi(v)$, and then it checks if $\ensuremath{P}$ satisfies $\varphi(v)$,
i.e., if $(\mathit{init}(v), \mathit{next}(v, v'))\models_{\mathit{CTL}} \varphi(v)$.
The method first generates a set of forall-exists quantified Horn constraints
with well-foundedness conditions by exploiting the syntactic structure
of the CTL formula $\varphi(v)$.
It then solves the generated set of Horn constraints by applying an
off-the-shelf solving engine \textsc{E-HSF}\xspace~\cite{ehsf} for such
constraints.
We claim that $\ensuremath{P}$ satisfies $\varphi(v)$ if and only if
the generated set of Horn constraints has a solution.
We demonstrate the practical applicability of the method by presenting
experimental evaluation using examples from the PostgreSQL database
server, the SoftUpdates patch system, the Windows OS kernel.

The rest of the paper is organised as follows.
We start by summarising the syntax and semantics of CTL and by giving a brief
introduction to forall-exists quantified Horn constraints and their
solver \textsc{E-HSF}\xspace in Section~\ref{sec:prelims}.
In Section~\ref{sec:proof-system}, we present our CTL proof system
that generates a set of forall-exists quantified Horn constraints for
a given verification problem.
We illustrate application of the proof rules on an example in
Section~\ref{sec:cons-gen}.
The experimental evaluation of our method is given in
Section~\ref{sec:eval}.
Finally, we present a brief discussion on related work in
Section~\ref{sec:rel-work} and concluding remarks in
Section~\ref{sec:concl}.

\section{Preliminaries}
\label{sec:prelims}
\subsection{CTL basics}

In this section, we review the syntax and the semantics of the logic
CTL following~\cite{KestenTCS95}.
Let $\mathcal{T}$ be a first order theory and $\models_{\mathcal{T}}$ denote its
satisfaction relation that we use to describe sets and relations
over program states.
Let $c$ range over assertions in $\mathcal{T}$.
A CTL formula $\varphi$ is defined by the following grammar using
the notion of a path formula~$\phi$.
\begin{equation*}
  \begin{array}[t]{@{}r@{\;::=\;}l@{}}
  \varphi &
    c \mid
    \varphi \land \varphi  \mid
    \varphi \lor \varphi   \mid
    \pathA \, \phi \mid
    \pathE \, \phi \\ [\jot]
    \phi & \ltlNext \varphi \mid \ltlG \varphi \mid \varphi \ltlU \varphi
  \end{array}
\end{equation*}
$\ltlNext$, $\ltlG$, and $\ltlU$ are called temporal operators, and
$\pathA$ and $\pathE$ are called path quantifiers.
A CTL formula whose principal operators are a pair QT, where Q is a
path quantifier and T is a temporal operator, and which does not
contain any additional temporal operators or path quantifiers is
called a basic CTL formula.
As usual, we define  $\ltlF \varphi = (\mathit{true}~ \ltlU \varphi)$.
The satisfaction relation $\ensuremath{P}\models \varphi$ holds if and only
if for each $s$ such that $\mathit{init}(s)$ we
have~$\sat{\ensuremath{P}}{s}{\varphi}$.
We define $\sat{\ensuremath{P}}{s}{\varphi}$ as follows using an auxiliary
satisfaction relation $\sat{\ensuremath{P}}{\pi}{\phi}$.

\begin{equation*}
  \begin{array}[t]{@{}l@{\text{ iff }}l@{}}
    \sat{\ensuremath{P}}{s}{c}
    &
    s \models_{\mathcal{T}} c \\[\jot]
    \sat{\ensuremath{P}}{s}{\varphi_1 \land \varphi_2}
    &
    \sat{\ensuremath{P}}{s}{\varphi_1} \text{ and }
    \sat{\ensuremath{P}}{s}{\varphi_2}\\[\jot]
    \sat{\ensuremath{P}}{s}{\varphi_1 \lor \varphi_2}
    &
    \sat{\ensuremath{P}}{s}{\varphi_1} \text{ or }
    \sat{\ensuremath{P}}{s}{\varphi_2}\\[\jot]
    \sat{\ensuremath{P}}{s}{\pathA\, \phi}
    &
    \text{for all $\pi \in \computations{\ensuremath{P}}{s}$ holds }
    \sat{\ensuremath{P}}{\pi}{\phi} \\[\jot]
    \sat{\ensuremath{P}}{s}{\pathE\, \phi}
    &
    \text{exists $\pi \in \computations{\ensuremath{P}}{s}$ such that }
    \sat{\ensuremath{P}}{\pi}{\phi} \\[\jot]
    \sat{\ensuremath{P}}{\pi}{\ltlNext \varphi}
    &
    \pi = s_1, s_2, \ldots \text{ and }
    \sat{\ensuremath{P}}{s_2}{\varphi} \\[\jot]
    \sat{\ensuremath{P}}{\pi}{\ltlG \varphi}
    &
    \pi = s_1, s_2, \ldots \text{for all $i\geq 1$ holds }
    \sat{\ensuremath{P}}{s_i}{\varphi} \\[\jot]
    \sat{\ensuremath{P}}{\pi}{\varphi_1 \ltlU \varphi_2}
    &
    \begin{array}[t]{@{}l@{}}
      \pi = s_1, s_2, \ldots
      \text{ and exists $j\geq 1$ such that }\\[\jot]
      \sat{\ensuremath{P}}{s_j}{\varphi_2} \text{ and }
      \sat{\ensuremath{P}}{s_i}{\varphi_1} \text{ for } 1 \leq i < j
    \end{array}
  \end{array}
\end{equation*}
In this paper, we represent a satisfaction relation $\ensuremath{P}\models
\varphi$ by the relation $\ensuremath{P}\models_{\mathit{CTL}} \varphi$ to
explicitly indicate that $\varphi$ is a CTL formula.
We call such relation a CTL satisfaction, and $\varphi$ is said to be
its formula.

\subsection{The solving algorithm \textsc{E-HSF}\xspace}
\label{subsec-ehsf}

Our proof rules are automated using the \textsc{E-HSF}\xspace engine for resolving
forall-exists Horn-like clauses extended with well-foundedness
criteria.

We skip the syntax and semantics of the clauses targeted by this
system --- see \cite{ehsf} for more details.
Instead, we illustrate these clauses with the following example:
\begin{equation*}
    \begin{array}[t]{@{}l@{\qquad}l@{}}
      x \geq 0 \rightarrow \exists y: x \geq y \land \mathit{rank}(x, y), &
      \mathit{rank}(x, y) \rightarrow \mathit{ti}(x, y),\\[\jot]
      \mathit{ti}(x, y) \land \mathit{rank}(y, z) \rightarrow \mathit{ti}(x,
      z), &
      \mathit{dwf}(ti).
\end{array}
\end{equation*}

Intuitively, these clauses represent an assertion over the interpretation of
``query symbols'' $\mathit{rank}$ and~$\mathit{ti}$ (the predicate
$\mathit{dwf}$ represents disjunctive well-foundedness, and is not a
query symbol).
The semantics of these clauses maps each predicate symbol
occurring in them into a constraint over~$v$.
Specifically, the above set of clauses has a solution that maps both
$\mathit{rank}(x, y)$ and $\mathit{ti}(x, y)$ to the  constraint  $(x
\geq 0 \land y \geq x-1)$.

\textsc{E-HSF}\xspace resolves clauses like the above using  a CEGAR scheme to
discover witnesses for existentially quantified variables.
The refinement loop collects a global constraint that declaratively
determines which witnesses can be chosen.
The chosen witnesses are used to replace existential quantification,
and then the resulting universally quantified clauses are passed to a
solver for such clauses.
At this step, we can benefit from emergent tools in the area of
solving Horn clauses over decidable theories, e.g.,
HSF~\cite{GrebenshchikovTACAS12} or $\mu$Z~\cite{muz}.
Such a solver either finds a solution, i.e., a model for uninterpreted
relations constrained by the clauses, or returns a counterexample,
which is a resolution tree (or DAG) representing a contradiction.
\textsc{E-HSF}\xspace turns the counterexample into an additional constraint on the
set of witness candidates, and continues with the next iteration of
the refinement loop.
Notably, this refinement loop conjoins constraints that are obtained
for all discovered counterexamples.
This way \textsc{E-HSF}\xspace guarantees that previously handled counterexamples
are not rediscovered and that a wrong choice of witnesses can be mended.

For the existential clause above, \textsc{E-HSF}\xspace introduces a
witness/Skolem relation $\mathit{rel}$ over variables $x$ and
$y$, i.e., $x\geq0 \land \mathit{rel}(x,y) \rightarrow x \geq y \land
\mathit{rank}(x, y)$.
For each $x$ such that $x\geq0$, we require the skolem relation to
provide the corresponding value for $y$, i.e., we require all such
$x$ is in the domain of the Skolem relation.
This is encoded by an additional clause $x\geq0 \rightarrow \exists y:
\mathit{rel}(x,y)$.
In the \textsc{E-HSF}\xspace approach, the search space of a skolem relation
$\mathit{rel}(x,y)$ is restricted by a template function
$\funTemplateOf{\mathit{rel}}{x,y}$.
In general, \textsc{E-HSF}\xspace requires such template functions to be given by
the user.

\section{Proof system}
\label{sec:proof-system}

Our CTL verification method encodes the verification problem as a problem of
solving forall-exists quantified Horn constraints with well-foundedness
conditions.
This is done by applying a proof system that consists of various proof
rules for handling different kinds of CTL formulas.
This proof system is based on a deductive proof system for CTL*
from~\cite{KestenTCS95} which is adapted in this work to be suitable
from the perspective of constraint generation for a CTL satisfaction.

Given a transition system $(\mathit{init}(v),\mathit{next}(v,v'))$ and a CTL
formula $\varphi(v)$, the appropriate proof rules are used from the
proof system to generate the corresponding set of Horn constraints for
the CTL satisfaction $(\mathit{init}(v), \mathit{next}(v, v'))\models_{\mathit{CTL}} \varphi(v)$.
There are two sets of proof rules in the proof system.

\subsection{Proof rules for decomposition}

These proof rules are applied recursively to a CTL satisfaction whose
formula is neither an assertion nor a basic CTL formula.
The proof rules decompose the given CTL formula into new
sub-formulas by following the nesting structure of the formula.
Then, the original satisfaction is reduced to new satisfactions over the
new sub-formulas and a Horn constraint relating the new
satisfactions.

There are different proof rules depending on the outermost operator
of the formula.
One case is when the given formula $f(\psi(v))$ nests another
formula $\psi(v)$ such that the outermost operator $f$ is a pair of a
temporal path operator and a unary temporal state operator, i.e., $f
\in \{AX, AG, EX, EG\}$.
The corresponding proof rule $\textsc{RuleCtlDecompUni}\xspace$ is given in
Figure~\ref{fig-ctl-proof-rule-decompUni} that shows how such satisfactions
are decomposed.
\begin{figure}[h]
  \makeFramedRule{Find an assertion $q(v)$ such that:}{
    (p(v), \mathit{next}(v, v')) \models_{\mathit{CTL}} f(q(v)) \quad (q(v), \mathit{next}(v,
    v')) \models_{\mathit{CTL}} \psi(v)}{
    (p(v), \mathit{next}(v, v'))\models_{\mathit{CTL}} f(\psi(v))}
  \caption{Proof rule \textsc{RuleCtlDecompUni}\xspace}
  \label{fig-ctl-proof-rule-decompUni}
\end{figure}
Another case is when the given formula has a structure $f(\psi_1(v),\
\psi_2(v))$ nesting the formulas $\psi_1(v)$ and $\psi_2(v)$ such that
the outermost operator $f$ is either a pair of a temporal path
operator and the state operator until or a disjunction/conjunction, i.e., $f
\in \{AU, EU, \land, \lor\}$.
Note that when $f$ is $\land$ (resp. $\lor$), the given formula
$f(\psi_1(v),\ \psi_2(v))$ corresponds to $\psi_1(v)\land
\psi_2(v)$ (resp $\psi_1(v) \lor \psi_2(v)$).
The corresponding proof rule $\textsc{RuleCtlDecompBin}\xspace$ is given in
Figure~\ref{fig-ctl-proof-rule-decompBin} that shows how such satisfactions
are decomposed.
\begin{figure}[h]
  \makeFramedRule{Find assertions $q_1(v)$ and $q_2(v)$
    such that:}{
    p(v) \rightarrow f(q_1(v), q_2(v)), \\
    (q_1(v), \mathit{next}(v, v')) \models_{\mathit{CTL}} \psi_1(v)  \quad (q_2(v),
    \mathit{next}(v, v')) \models_{\mathit{CTL}} \psi_2(v)}{
    (p(v), \mathit{next}(v, v'))\models_{\mathit{CTL}} f(\psi_1(v),
    \psi_2(v))
  }
  \caption {Proof rule \textsc{RuleCtlDecompBin}\xspace}
  \label{fig-ctl-proof-rule-decompBin}
\end{figure}

\subsection{Proof rules for constraints generation}

This set of proof rules is applied to a CTL satisfaction whose formula
is either an assertion or a basic CTL formula.
Any CTL satisfaction can be decomposed into a set of such simple CTL
satisfactions by applying the proof rules from the previous section.
The next step will be to generate forall-exists quantified Horn constraints
(possibly with well-foundedness condition) that constrain a set of
auxiliary assertions over program states.

The simplest of all is the proof rule \textsc{RuleCtlInit}\xspace, see
Figure~\ref{fig-ctl-proof-rule-init}, which is applied when the CTL
formula is an assertion. \\
\begin{minipage}{.48\textwidth}
\begin{figure}[H]
  \makeFramedRule{}{
    p(v) \rightarrow \psi(v)
  }{
    (p(v), \mathit{next}(v, v')) \models_{\mathit{CTL}} \psi(v)
  }
  \caption{Proof rule \textsc{RuleCtlInit}\xspace}
  \label{fig-ctl-proof-rule-init}
\end{figure}
\end{minipage} %
\hspace{1 em}
\begin{minipage}{.48\textwidth} %
\begin{figure}[H]
  \makeFramedRule{}{
    p(v) \rightarrow \exists v': \mathit{next}(v,v') \land q(v')
  }{
    (p(v), \mathit{next}(v,v')) \models_{\mathit{CTL}} EX~q(v)
  }
  \caption{Proof rule \textsc{RuleCtlEX}\xspace}
  \label{fig-ctl-proof-rule-EX}
\end{figure}
\end{minipage}
\vspace{2 em}\\
The proof rules \textsc{RuleCtlEX}\xspace (see Figure~\ref{fig-ctl-proof-rule-EX}),
\textsc{RuleCtlEG}\xspace (see Figure~\ref{fig-ctl-proof-rule-EG}), and  \textsc{RuleCtlEU}\xspace
(see Figure~\ref{fig-ctl-proof-rule-EU}) are applied for generating
Horn constraints when the CTL satisfaction problem has a basic CTL
formula with existential path operator. \\
\begin{minipage}{.4\textwidth}
\begin{figure}[H]
  \makeFramedRuleSS{Find an assertion $\mathit{inv}(v)$ such that:}{
    p(v) & \rightarrow & \mathit{inv}(v)\\
    \mathit{inv}(v) & \rightarrow & \exists v': \mathit{next}(v,v') \land \mathit{inv}(v')\\
    \mathit{inv}(v) & \rightarrow & q(v)
  }{
    (p(v), \mathit{next}(v,v')) \models_{\mathit{CTL}} EG~q(v)
  }
  \caption{Proof rule \textsc{RuleCtlEG}\xspace }
  \label{fig-ctl-proof-rule-EG}
\end{figure}
\end{minipage} %
\hspace{1 em}
\begin{minipage}{.56\textwidth} %
\begin{figure}[H]
  \makeFramedRuleSS{Find assertions $\mathit{inv}(v)$ and $\mathit{rank}(v,v')$ such that: }{
        p(v) & \rightarrow & \mathit{inv}(v)\\
        \mathit{inv}(v) \land \neg r(v) &  \rightarrow &  q(v) \land \exists v':  \mathit{next}(v,v') ~\land \\[\jot]
                 & & \mathit{inv}(v') \land \mathit{rank}(v,v') \\[\jot]
       & \mathit{wf}(\mathit{rank})
  }{
    (p(v), \mathit{next}(v,v')) \models_{\mathit{CTL}} EU(q(v),r(v))
  }
  \caption{Proof rule \textsc{RuleCtlEU}\xspace}
  \label{fig-ctl-proof-rule-EU}
\end{figure}
\end{minipage}
\vspace{2 em}\\

Similarly, the proof rules \textsc{RuleCtlAX}\xspace (see Figure~\ref{fig-ctl-proof-rule-AX}),
\textsc{RuleCtlAG}\xspace (see Figure~\ref{fig-ctl-proof-rule-AG}), and  \textsc{RuleCtlAU}\xspace
(see Figure~\ref{fig-ctl-proof-rule-AU}) are applied for generating
Horn constraints when the CTL satisfaction has a basic CTL formula with
universal path operator.

\begin{minipage}{.48\textwidth}
\begin{figure}[H]
  \makeFramedRuleSS{}{
    p(v) \land \mathit{next}(v,v') & \rightarrow & q(v')
  }{
    (p(v), \mathit{next}(v,v')) \models_{\mathit{CTL}} AX~q(v)
  }
  \caption{Proof rule \textsc{RuleCtlAX}\xspace}
  \label{fig-ctl-proof-rule-AX}
\end{figure}
\end{minipage} %
\hspace{1 em}
\begin{minipage}{.48\textwidth} %
\begin{figure}[H]
  \makeFramedRuleSS{Find an assertion $\mathit{inv}(v)$ such that:}{
    p(v) & \rightarrow & \mathit{inv}(v)\\
    \mathit{inv}(v) \land \mathit{next}(v,v') & \rightarrow & \mathit{inv}(v')\\
    \mathit{inv}(v) & \rightarrow & q(v)
  }{
    (p(v), \mathit{next}(v,v')) \models_{\mathit{CTL}} AG~q(v)
  }
  \caption{Proof rule \textsc{RuleCtlAG}\xspace}
  \label{fig-ctl-proof-rule-AG}
\end{figure}
\end{minipage}
\vspace{2 em}\\
\begin{figure}[h]
  \makeFramedRule{Find assertions $\mathit{inv}(v)$ and $\mathit{rank}(v,v')$ such that: }{
    p(v) \rightarrow \mathit{inv}(v)\\
    \mathit{inv}(v) \land \neg r(v) \land \mathit{next}(v,v') \rightarrow
    \begin{array}[t]{l}
      q(v) \land \mathit{inv}(v') \land \mathit{rank}(v,v')
    \end{array}\\
    \mathit{wf}(\mathit{rank}).
  }{
    (p(v), \mathit{next}(v,v')) \models_{\mathit{CTL}} AU(q(v), r(v))
  }
  \caption{Proof rule \textsc{RuleCtlAU}\xspace}
  \label{fig-ctl-proof-rule-AU}
\end{figure}

Our proof system is not exhaustive in terms of having proof rules for
all kinds of basic CTL formulas.
However, we utilize equivalence between CTL formulas to generate
Horn constraints for basic CTL formulas whose proof rules are not
given in the proof system.
For example, the equivalence between the formulas
$EU(\mathit{true},q(v))$ and $EF(q(v))$ can be used to reduce the CTL
satisfaction problem $(p(v), \mathit{next}(v,v')) \models_{\mathit{CTL}} EF(q(v)$ into
$(p(v), \mathit{next}(v,v')) \models_{\mathit{CTL}} EU(true, q(v))$.

\section{Related work}
\label{sec:rel-work}

Verification of properties specified in temporal logics such as CTL
has been extensively explored for finite-state
systems\cite{Kupferman2000, Burch1990, Clarke02treelikeCEX,
  Clarke1983AVF}.
There has also been studies on the verification of CTL properties for
some restricted types of infinite-state systems.
Some examples are pushdown processes \cite{Song2013, Song2011, Walukiewicz2000},
pushdown games \cite{walukiewicz2001pushdown},
and parameterised systems \cite{Emerson1996}.
For such restricted systems, the standard procedure is to abstract the
infinite-state system model into finite-state model and
apply the known methods for finite-state systems.
But existing abstraction methods usually do not allow reliable
verification of CTL properties where alternation between universal and
existential modal operators is common.
Many methods of proving CTL properties with only universal path
quantifiers are known\cite{Chaki2005, Cook2012TPV}.
 There also a few methods mainly focused on proving branching-time
properties with only existential path quantifiers.
One example is the tool Yasm \cite{GurfinkelWC06} which implements a
proof procedure aimed primarily at the non-nested existential subset of
CTL.
There are also known techniques for proving program
termination~\cite{Bradley05polyrankingfor, TerminatorPLDI06}
(resp. non-termination~\cite{TNTPOPL08}) which is equivalent with
proving the CTL formula $AF~false$ (resp. $EG~true$).

Banda et al.~\cite{Banda2010CAS} proposed a CTL verification approach
for infinite state reactive systems based on CLP and abstraction of a
CTL semantic function.
An automatic proof method that supports both universal and existential
branching-time modal operators for (possibly infinite-state) programs
is proposed in by Cook et al.~\cite{CookPLDI13}.
Cook's approach is based on reducing existential reasoning to universal
reasoning when an appropriate restriction is placed on the the
state-space of the system.
While this approach comes close to our approach, the refinement
procedure for state-space restrictions may make
incorrect choices early during the iterative proof search.
These choices may limit the choices available later in the search
leading to  failed proof attempts in some cases.

redpajama_set_name: RedPajamaArXiv


If you look real close you can see some grouse roosting in the tree still. It usually takes them a while to get going on these cold mornings. Taken 1/29/2007.
The pair of Sandhill cranes that have been hanging around here. Last year I seen their baby around but this year I don't see one. It must not have made it. Hopefully they will have better luck next year. Taken 9/5/2006.
This herd of turkeys caught my eye. There are a large number of all game birds around this year. It must have been a good year for them. That and there is not many coyotes around to prey on them. Taken 8/31/2006.
I caught this little fella chewing on a pine cone while I was checking a water hole. I had noticed for quite a while that something had been chewing on the tree but wasn't sure what. Turns out it wasn't chewing the tree but chewing the pine cones. My Darling Wife told me it was a chipmunk. I wasn't sure and did some research and discovered it to be a Red Squirrel. Taken 8/14/2006.
These little baby grouse weren't sure where to go after the fire. They were wandering around half lost. There mother was there but she was confused to. Taken 8/1/2006.
A picture My Darling Wife got of one of the fox hanging around the place. As long as they leave me alone I will leave them alone but I keep waiting for them to go after My Darling Wife's chickens. Then I will have to thin the population down. Taken 7/24/2006.
On the left of this picture you see my boy out for his morning walk climbing the hills and rocks for fun. I know it's hard to see but there is a fox on the right hand side of the picture watching him. There is a den of fox on the hill and they are so used to him, they aren't very scared anymore. Best viewed large to see the fox. Taken 6/23/2006.
I spooked up two antelope kids (calves, fawns?) yesterday on my way home. I finally saw mom up on the hill a little ways away. They ran up to her. Taken 6/22/2006.
The cranes are back in the country. There has been a pair nesting here for about 3 years now and they keep coming back. They overflew us twice while feeding so I assume they are letting us know they are here. Taken 4/7/2006.
Sharptail grouse foraging for food during the light snow storm on Thursday. There were quite a few more in the area that I didn't get a picture of. I have never seen so many around during the winter. Maybe the coyotes will bother them and leave my calves alone.
I saw something yesterday I haven't seen in years. A XXXXXXXX. I saw them as a kid sometimes but even seeing one like I did was neat. Hopefully I will begin to see a few more around. It wouldn't hurt my feelings.
By the way, I never admit to seeing a critter that is on or might be listed on the endangered species list. Admitting to it is a good way for the Government to come down on you and control what you can and can't do with your property. That's why I won't identify what I saw. Plausible deniability.
The Prickly Pear Cactus are starting to bloom. Pretty, but not fun. Taken 6/10/2007.


The NCAA brings more action today as the Villanova Wild Cats will clash with the Canisius Golden Griffins for a place in the semifinals Villanova fell 76-68 in overtime at home to Furman Saturday in their last game. On the other side, Canisius was lost with a score of 93-61 on the road by #14 Florida State in their last game Monday night.
The Wildcats are the team that is defending the title but it seems that they have a slight drop of form lately.
The Wildcats are in a transition process as they are aiming to find the right balance in replacing key players from last year's title team.
On the defensive side of the game, their average stands at 69.8 points per game so far this season.
Phil Booth is the leader of the team this season as the record stands at 17.3 points per game.
Villanova is hitting 10.3 three-pointers a game but hit only 32 per cent of their attempts. The Wildcats are struggling at the line, converting only 66 per cent of their chances.
The Golden Griffins had a good start of the year but they have lost two since that opening. They were beaten fair and square by Florida State on Monday and it seems that they will need to regroup in order to get something out of this game. However, on the bright side, Malik Johnson had a solid performance as he scored 20 points in this defeat.
On the offensive side of the game, the Griffins have an average record of 69.7 points per game. Also, they have an average of 11.7 assists per game so far this season.
On the defensive side of the game, they have been conceding an average of 80.3 points per game.
Takal Molson is the leader of this time as he is scoring an average of 21.3 points combined with 5.3 rebounds per game.
Villanova suffered a couple of defeats at the hands of Michigan and Furman. They have dropped their form lately but they are still a very good team and the defending champion. They have the quality and I believe that Canisius does not have the quality to match them at the moment. That is why I expect a Villanova win in this game.


View of Amer Fort near Jaipur, in India's Rajasthan State.
A stone chariot at the Vittala temple complex at Hampi in India's Karnataka State.
A builder on a site in Sarojini Nagar market, New Delhi.
India became the Commonwealth's first Republic on 26 January 1950.
The longest-standing of India's three national holidays, marking the end of the British Raj.


text:
Prison Break 2005: Season 2
Prison Break 2005
Prison Break: Season 2
Prison Break Season 2 – In season two, Michael, Lincoln and six other inmates, including pickpocket Tweener and the mentally unstable Haywire, have ultimately escaped from Fox River. Once outside the prison walls, however, the escape truly begins as the convicts race for their lives while trying to avoid capture by the authorities. The pursuers are led by FBI agent Alexander Mahone, who is haunted by his own demons; vengeful prison guard Captain Brad Bellick, who, driven by his own personal vendetta, will also stop at nothing until the escapees are captured or killed; and Secret Service Agent Paul Kellerman, who, under President Reynolds' orders, will do anything to keep the truth about the conspiracy very much a secret. – Stream Prison Break Season 2 Online for Free – Watch Prison Break Full Season 2 Free – OnionPlay Official
Prison Break: Season 2 Streaming Online | Watch Prison Break: Season 2 Online
Prison Break: Season 2 HD Stream | Prison Break: Season 2 Watch HD Stream | Prison Break: Season 2 Online
Sona Apr. 02, 2007
Fin Del Camino Mar. 26, 2007
Panama Mar. 19, 2007
Sweet Caroline Mar. 05, 2007
Wash Feb. 26, 2007
Bad Blood Feb. 19, 2007
Chicago Feb. 05, 2007
The Message Jan. 29, 2007
John Doe Jan. 22, 2007
The Killing Box Nov. 27, 2006
Disconnect Nov. 20, 2006
Bolshoi Booze Nov. 13, 2006
Rendezvous Nov. 06, 2006
Unearthed Oct. 30, 2006
Dead Fall Oct. 23, 2006
Buried Oct. 02, 2006
Subdivision Sep. 25, 2006
Map 1213 Sep. 18, 2006
First Down Sep. 11, 2006
Scan Sep. 04, 2006
Otis Aug. 28, 2006
Manhunt Aug. 21, 2006

redpajama_set_name: RedPajamaCommonCrawl


text:
> 'Threat of imminent attack on US Jews is real'
'Threat of imminent attack on US Jews is real'
Deputy Homeland Security Secretary paints grim picture of Jewish communities' vulnerability to terrorism, says leaders not doing enough.
American Jews US Jews Terror Threat
Illustration Thinkstock
JTA - Painting a grim picture of Jewish vulnerability in the United States, a top U.S. security official said that the vast majority of funds earmarked to secure non-profits goes to Jewish institutions because their need is most acute.
Alejandro Mayorkas, the Deputy Homeland Security Secretary, speaking Wednesday to the Orthodox Union's annual leadership mission to Washington, said rising extremism in the United States and its threat to the Jewish community keeps him awake at night.
He said the threat had shifted in the last year from the relatively small number of Americans who were radicalized overseas, to homegrown extremists whom the Islamic State terrorist group had reached through the Internet. The FBI was tracking more than one thousand suspected extremists across the United States, and they were to be found in all 50 states, he said.
"They find great access to a radicalizing Islam" on the web, Mayorkas said of the homegrown extremists. "They find what they believe is purpose and meaning in their life."
The nonprofit security grants approved by Congress — $20 million this year — "preeminently" go to the Jewish community," Mayorkas said.
"The need is most acute in the Jewish community because of the ascension of anti-Semitism and hate crimes we see," Mayorkas said.
In past years, more than 90 percent of the funds have gone to Jewish groups. The FBI reported last year that 57 percent of reported anti-religious hate crimes had an anti-Jewish bias.
Mayorkas challenged Jewish leaders to raise awareness about potential threats, to hire better-trained security staff, to add protections at Jewish institutions, to train the community in how to respond to an active shooter, to establish relationships with local police and to increase cyber security. He said hackers could access personal information about Jewish children who are affiliated to Jewish organizations and use it to target them.
"This is real," he said. "This is real. We must treat the imminence" – of an act of terrorism – "as real."
He said his trepidation was in part formed by his upbringing. Mayorkas' mother is a Romanian Jew who survived the Holocaust and who moved to Cuba after marrying a Cuban Jew. They moved to the United States after the Cuban revolution.
Among the things that "keep me up at night," he said, was the threat to "my community," the Jewish community, he said.
"I come from a tradition of a lack of security instilled in me as a very young person," he said.
He said extremism was rising across the world.
"We live in a time of increasing concern, not diminishing concern," Mayorkas said. "If one takes a look at some of the political leaders gaining ascension across the globe, it does not give me comfort with respect to the Jewish community," he said, stressing that he was referring to foreign leaders and not domestic politicians.
Mayorkas also urged leaders to contact Paul Goldenberg, who heads the Secure Community Network, the security arm of the Jewish Federations of North America, to learn more about how to secure their institutions.
Separately, Goldenberg was reappointed Wednesday to the Department of Homeland Security's advisory council, which consults with Mayorkas and Homeland Security Secretary Jeh Johnson. Goldenberg was first appointed to the council in 2013.


text:
Shore Voices: Hope for our future
Though some college students seem to know more pop culture than current events or U.S. history, others are tuned in.
Shore Voices: Hope for our future Though some college students seem to know more pop culture than current events or U.S. history, others are tuned in. Check out this story on delmarvanow.com: https://www.delmarvanow.com/story/opinion/editorials/2016/02/05/different-views-caucus-20160207/79873418/
Susan Parker, Salisbury Daily Times Published 1:02 p.m. ET Feb. 5, 2016 | Updated 6:48 a.m. ET Feb. 6, 2016
University of Maryland Eastern Shore is one of Maryland's Historically Black Colleges and Universities. (Photo: File photo)
I recently saw a video clip on social media that featured a young woman, presumably a university student, interviewing other students on an unidentified campus somewhere (I know, way too vague). It was disturbing, probably by design, because the students were asked to answer some simple questions, but by and large they could not provide accurate responses and in many cases, no answer at all beyond "I have no idea" or "What are you talking about?"
I hope it was a spoof. I hope these kids had been coached ahead of time to give silly answers like that. I hate to think they were really as clueless as they appeared to be.
Perhaps you saw that clip, too. The first question was "Who won the Civil War?" Responses ranged from "What war? Was that in the 1960s?" to "Uh, the South?" or "Tell me who was in it and maybe I can answer" and "America?"
Only one of about five students who appeared on the video were able to identify our vice president in 2016, and that was with some prompting from the interviewer.
They all had immediate and apparently accurate answers to questions about reality TV stars, they knew who was married to actor Brad Pitt and other entertainment-related questions that I was clueless about.
My initial reaction was "and these are our best and brightest, the kids who are accepted to universities today?"
So what gives me hope in light of this?
This is the second week I have invited students in an advanced English class at University of Maryland Eastern Shore to participate in my Sunday "Different Views" column. The first time, the question tackled the Planned Parenthood video debacle. This week it's the influence of the Iowa caucus on their voting decisions.
Both times, they have provided a wide range of thoughtful answers. Yes, their professor did initiate a class discussion before they wrote their answers, but their answers reflect more than what you could possibly learn in a brief class discussion of a complex issue. The responses are well-crafted, requiring no more editing than is done for veteran participants, most of whom are retired or approaching that milestone.
If you haven't read this column lately, have a look this Sunday. Most will appear in the print edition of Voices on Sunday, and all will be available online.
The thoughtful comments made by these young people who are about to enter the workforce and the adult world will surely make you feel better about our future — even if you disagree with them on a political level. They are a refreshing addition to our Different Views panel of writers.
Read or Share this story: https://www.delmarvanow.com/story/opinion/editorials/2016/02/05/different-views-caucus-20160207/79873418/


text:
Home Construction & Engineering JMS announces opening of new office in Mayfair
JMS announces opening of new office in Mayfair
27/02/2019 - JMS Consulting Engineers
Local based engineering company JMS, has announced the opening of a new office in London's Mayfair, bringing the total JMS offices in the UK and Europe to 9.
The new office will initially provide the in-house design services of Civil & Structural Engineering. With projects already completed at the Shaftesbury Theatre, Maddox Street and the Trocedero, Mayfair is a strategically important office and is in keeping with the company's continuous desire to support their clients with a hands-on, local service.
Daniel Staines, Managing Director at JMS commented; "We are very pleased to announce the opening of our new Mayfair office, which highlights the success we have achieved through our dedication and ongoing commitment to London and the surrounding areas.
The decision to expand our presence into Mayfair is a logical step in our business strategy, there are so many exciting opportunities to explore in this area, we look forward to continuing to offer our specialised services to this unique and diverse capital".
For further information visit the JMS Group website
The challenges of working for a UK Company whilst living overseas
Re: JMS Consulting Engineers
JMS celebrate win at East Midlands Celebrating Construction Awards
Did you know: Only 12.37% of all engineers in the UK are women...
Re: Scottish Power Renewables
Drain Doctor aids DIY SOS latest project
Re: Anglia Drain Doctor


text:
James Franco Full Frontal Nudity; Cory Booker Looking For Gay Vote?
James Franco Full Frontal Nudity
Someone sent me this link, and since it's Labor Day Weekend I thought I would share. Can't post the photos here on this blog, but the link is safe and it works very well.
Hotness career student, and all around renaissance man James Franco derives many a pleasure from teasing his gay and straight fans alike. We will never forget his Flaunt derriere cover and be forever grateful for it.
But this here photo is one of the best-est gift that could be extended to his legions of fans worldwide. See more pics of Franco after the jump!
Franco is no stranger to nudity on screen – Milk pool scene immediately jumps to mind – but full frontal has alluded all of us waiting for the final frontier to be showcased. Some lucky shutter-bug, however, apparently caught this very missing link while Franco aired out his family jewels on some beach, reaping the benefits some of us would pay a hefty price to witness first hand.
This photo actually supports one of my theories about male full frontal nudity in films, and with well known actors. It's obvious James Franco has nothing to hide, but this could be the reason why we don't see more full frontal nudity with male actors. I know they can make it look real with stand-ins. However, no man wants to go there unless it's absolutely necessary.
Stand-ins are not good for the ego.
Cory Booker Looking For Gay Vote?
There's been some talk recently about the NJ Democratic candidate running for the Senate, Cory Booker, and whether or not he's gay. I posted this earlier this week. It was the topic of discussion in a few places I went yesterday. And now it seems he's being accused of being ambiguous about whether or not he's gay so he can allegedly snatch up the gay vote.
The Senate campaign of Newark Mayor Cory Booker said his Republican rival was "bigoted" for saying that Booker was "acting ambiguous" in an effort to attract gay votes.
Booker's team was reacting to comments by Republican Steve Lonegan, a conservative who is trailing badly in polls.
Lonegan, who is known for his blunt style, seemed to raise old rumors that Booker might be gay and told the conservative Newsmax TV that recent Booker comments where he said he doesn't care if people do think he is gay because "I want to challenge people on their homophobia" were "weird."
This entire discussion just shows how little the mainstream actually knows about gay men, and how the gay stereotype is perpetuated all the time. It seems to be a given that all gay men are liberal Democrats, as if this is part of their birthright. And just because Cory Booker is a liberal Democrat who gay men "think" might be gay they will run out in droves to the voting booths just for that alone. And that's just not how it works.
The fact is not all gay men are liberal Democrats. Personally, I'm an independent. Not all gay men vote according to a candidate's sexuality. If I still lived in New Jersey I probably would vote for Cory Booker. But not because he "could" be gay, or because he's a Democrat. It's because I've seen what he's accomplished in the city of Newark and I'd like to see someone in Washington who can get results like that.
Women Who Love to Love Gay Romance; Indie Publishing
Instead of adding a link to the other post about the release of this book, I wanted to mention something for those who think indie publishing is simple in a separate post. This book was uploaded to Amazon around six o'clock this morning and I just received an e-mail verification that it went live a few minutes ago. Thankfully, Smashwords and allromanceebooks.com were faster to deal with. This is also why it's so hard to pinpoint an actual release time unless you have a web site of your own and sell the books from there.
In any event, this is the Amazon link.
Rainbow Award Jurors Thanks; Racism on Big Brother 15 Confronted
Rainbow Award Jurors Thanks
Each year the jurors who are part of the rainbow awards work very hard reading and rating books, so when I saw this note of thanks today I asked if I could have permission to post it here on the blog so readers can see what's going on behind the scenes. I have one good friend who I know is reading at least eight books, and others are reading even more. And it's nice to see that all this hard work is helping a cause in the long term.
Dear Jury,
I really want to thank you for all you have done and are doing, reading for the past 6 months, reading all the last minute entries, and be willing to read for the October/November for more than what you have initially agreed. That means a lot, but not only for the Rainbow Awards and the authors, that means that we were able to raise almost 6.000 dollars, and since my input is to not spend a lot of money to print the certificates to the winners (I'm sure they will be more than happy with a nice paper to frame), most of them will go to charity. I want to give you a feeling of what YOU have achieved: with $150 Ali Forney center provides temporary shelter to a kid for one week; with $500 a week they connect with these youth through Outreach Services, which include safe sex education, counseling, and services to help them off of the streets. I'm sure you are proud that we will be able to give them help.
Again, THANK YOU, Elisa
Racism on Big Brother 15 Confronted
I've posted about racism and gaycist comments on the TV reality show Big Brother before this summer, and what's been happening on Big Brother 15 this season seems to continue to devolve into a display of bullying and hate from certain individual players, Aaryn Gries and Amanda Zuckerman being two of the biggest bullies and racists in the house. There are others. In this article titled, Big Brother 15: A Cesspool of Homophobia and Racism you can read more. For those who don't know what a cesspool is, that's where waste water and human waste goes for people who live in rural areas. It's a dated term, because most have septic tanks, but it's also an appropriate example of what's been happening in BB15 this season.
And you have to understand that these people know they are being filmed 24 hours a day, nonstop. So it's either arrogance or stupidity or a combination of both.
Last night I watched the live eviction show and Aaryn Gries was finally voted out of the house, which meant she had to face Julie Chen at the end of the show before a live studio audience. I have to admit that I've been waiting for that all summer. Some of the shows were so vicious I had tears in my eyes. The moment Aaryn Gries walked out on the stage there was a mixed reaction from the audience, to which she didn't seem to react at first. Julie Chen asked the usual questions she normally asks each contest who has been voted off, and then she went into a few questions about Aaryn's racist comments that I won't mention here on this blog. You can see them yourself here.
This post is interesting. There are more examples of what has been said, too, you can find with a simple search.
CBS has little choice but to air the comments during the shows, since the situations are seen and heard on the show's live feed. The comments spread like wildfire over Twitter and other social media. The repercussions outside of the house are unknown to the house guests, but jobs have been lost and some people are clearly making their lives after the show more difficult.
The most interesting thing is that none of the players who have made the racial and anti-gay slurs have any idea what's been happening outside the Big Brother house all summer. Several have been fired from their jobs, and one was close to being fired last I'd read, as a result of this racism. And from what I saw last night by the way Aaryn reacted, she's in for a few more surprises when the season is over and she goes back home to Texas. At one point in last night's show she even blamed her comments on being from Texas, which I didn't buy at all. I know plenty of people who live in Texas and they aren't racists.
And what's going on with Amanda and that boyfriend of hers isn't worthy of posting anywhere. You have to wonder that if Amanda is the way she is openly, and her boyfriend on the show seems to support her, does that make him any less of a bully than she is?
As a side note, Julie Chen, an Asian American, handled the interview with Aaryn as a true professional, especially considering the fact that some of Aaryn's comments were directed toward Asian Americans.
FREE Excerpts Women Who Love to Love Gay Romance; Miss Richfield in Philly
Women Who Love to Love GR Release Day
Update: Link to Smashwords and here's one for Allromanceebooks.com Link
Today is the release day of my recent anthology, The Women Who Love to Love Gay Romance. When I began this project last January and put out the call for submissions I knew it wouldn't be a fast book to release. In other words, I wanted to take my time, gather the right stories and authors, and put together a book that will hopefully be entertaining and interesting for everyone. Each story has a strong plot, and each one is markedly different from the other. I've already written several posts about the book as things have cropped up since January, and here's a link to most of them.
In celebration of the release day for The Women Who Love to Love Gay Romance, I'd like to post a few excerpts from some of the stories. I still don't have a link yet to Amazon because it takes a while for the book to go live. But I will update when I get one very soon.
From Changing Curses by Li Blaine
By the time she turned sixteen, new carts buckled and broke the instant she placed her hand on them. By eighteen, each and every horse she mounted stumbled and became lame. At twenty-three, the weather found her and dried the fields. Crops withered during the harvest and streams flooded during the winter. The village was near starvation when Ilya finally set off alone. The sandy mountains of the outland became her home. Food was scarce and weight fell from her bones but still she lived. For years, she watched from the dusty hillside as life returned to the community, knowing she'd been to blame for what they had suffered.
From The Facilitator by Tilly Hunter
I work from home, drawing up designs for fancy dress costumes for a movie merchandising company. Jake is staying at my apartment temporarily while he looks for a new place. But the way things are going, he'll be moving in with his fella Will before long. I'll miss the company, but I'll be glad to stop hiding my romance books. I don't know why I hide them, really. I'm sure I wouldn't if they were straight-up erotica, but they're not. Generally they're kinky man-on-man smut; sometimes with fangs.
From The Courage to Jump by Oleander Plume
Lucy Larson was the pen name of one Brenda Suggins, age thirty, graduate of Merck County Community College, with a certificate in interior design. Which wasn't even worth the paper it was printed on since the closest thing she ever came to an interior design job was working in the drapery department at Sears. Instead, Brenda was a bank clerk by day and the secret writer of gay erotica by night. Her latest series, Brothers of the Crescent Moon, was very popular among young gay men, but lately, even more of her readers were heterosexual females. Reading about the exploits of two hot, long haired, muscular werewolves really got some women hot. The latest book in the series was highly anticipated and had already sold two thousand copies in pre-sales.
Lucy started writing erotica for fun, then at the urging of an old boyfriend (who later turned out to be gay) she sent one of her short stories to a publisher and her career took off from there. Of course only Lucy's publisher and her old boyfriend knew about her secret life. She kept it well hidden from friends and relatives. She couldn't even imagine the reaction she would get from her mother if she knew she was writing about gay sex. No, she could imagine and it was pretty ugly.
Miss Richfield in Philly
When I saw this on my local Philadelphia news channel last night I figured I would share with links. For those who don't know who Miss Richfield is, he's a well known female impersonator I first saw about twelve or thirteen years ago in Provincetown at the Crown and Anchor, and I've been following his act ever since. I don't typically follow that sort of thing unless it's something I think is really good. And for me that sort of entertainment is only good when it's done with camp, satire, and is so over the top you know you're not supposed to take it seriously. All you're supposed to do is have fun watching it. It really is an art.
In any event, there's a new TV commercial out where Miss Richfield is marketing toward the LGBT community to visit Philadelphia. The first time Miss Richfield did this was in 2004.
"Ten years ago, Philadelphia was proud to officially 'come out' as a gay-friendly destination when we invited LGBT travelers to visit," said Meryl Levitz, president and CEO of GPTMC. "With our new commercial, we're going beyond our history roots and reiterating our invitation, celebrating both the city's evolution into a premier destination and the LGBT community's progress over the last decade."
In the new 30-second spot, titled "Miss Richfield's Selfie Tour of Philadelphia," the flamboyant Miss Richfield 1981 embarks on a Philadelphia tour, visiting landmarks all over the city while snapping photos of herself-and some new buff friends-along the way. While wearing her red-white-and-blue, she starts at Independence Hall and the Liberty Bell; runs the Rocky steps yelling "Yo, Adrian!" at the Philadelphia Museum of Art; admires the views along the Schuylkill River; dines alfresco over food and wine; dances at a crowded nightclub; and finally, collapses onto a hotel room bed.
You can read more here. And this is a web site for Miss Richfield on Word Press. We live between New York and Philly and know both cities fairly well. There's really a lot to do in Philly, and it's always been gay friendly for those who are single, those who are couples, and those who would like to be a couple.
Women Who Love to Love Gay Romance; Freedom to Marry
Women Who Love to Love Gay Romance
I'm only posting a reminder that tomorrow, August 30th, is the release date for the anthology, The Women Who Love to Love Gay Romance. I'll post more tomorrow about it in detail, with a few excerpts, too. (Contributing authors, I will be in touch with you very soon with copies.)
And when I say that tomorrow is the release date, please take into consideration that I don't know a specific time when it will go live on Amazon. The book will be distributed in many places, but I like to put it on Amazon first because that's where I usually get most of my feedback. And I'm never exactly certain when it will go live after it's uploaded to Kindle. As soon as I have links, I'll put them up on tomorrow's post.
I've been posting about the Freedom to Marry organization for a long time now. You can read those posts here. In many ways Freedom to Marry has been my own personal catharsis because I'm living in PA where gay marriage is still not legal and my twenty year relationship with Tony has not been recognized like those in other states since the SCOTUS ruling. And not even in my own home town where I always thought the LGBT community set examples for others.
It's been a disillusioning week for all gay couples in New Hope, and what surprises me even more is that there are some gay people who are supporting the mayor's decision not to buck an immoral law and not to fight for equality to be on the right side of history. That kind of mind set just blows me away because it's political and not emotional. This is the main reason why I decided not to go to law school after I graduated from college and took my LSATs. When it comes to things like this I don't support or respect every single law, and I believe there are certain laws that need to be changed.
This is the latest from Freedom to Marry
This week has seen a flurry of activity supporting the freedom to marry in New Mexico. Three counties in New Mexico have been ordered by district court judges to end marriage discrimination and begin issuing marriage licenses to same-sex couples. County clerks in three additional counties have followed the lead of these rulings by issuing marriage licenses to same-sex couples in their own counties. These huge steps forward in New Mexico this week bring renewed urgency to why we need the freedom to marry uniformly across the state – and, ultimately, why we need the freedom to marry nationwide.
MensUnderWearStore.Com; New Hope Mayor No Gay Marriage; 2004 Marriage License Legal in NM
MensUnderWearStore.Com
I get interesting e-mails all the time from companies all over the world. Some I even like posting about with permission from the companies that send these e-mails. In this case I'm talking about mensunderwearstore.com, where they carry a line of underwear that's different from other places I've seen. The prices are not bad at all, and I own a few pairs myself.
The MensUnderwearStore.com team of photo experts recently shot Ryan Bertroche on location in St. Louis, MO. A native of Iowa, Ryan broke a sweat and kept things sizzling with his looks that resemble a young Kurt Russell. In addition to modeling the new Calvin Klein Athletic collection, Ryan also wore items from the Under Denim, Dry Touch and Fresh & Bright collections from Diesel.
Here are a few of Ryan's tasteful photos:
New Hope Mayor No Gay Marriage
In order to give you a better perspective about what's been going on in New Hope, where I live, located in southeastern, PA where same sex marriage is still illegal in spite of the SCOTUS ruling, here are a few more links, below. For those who don't know, Tony and I owned an art gallery in New Hope for ten years, and we've lived three miles away from downtown New Hope for over eleven years. Before that, we lived two miles from downtown New Hope in a town house community surrounded with gay neighbors. We've been together for twenty-one years and Tony is a lifelong native of Bucks County, PA. We didn't just move here to live near cookie cutter developments because they look nice. We didn't just move here because the schools are good. We live here because of the fact that there is a large LGBT community. What prompted that move happened while we were living in a more mainstream community about eight miles away, where an eight year old boy living next door to us asked his dad, "Why don't we get Christmas decorations like the two fags next door." We decided that neighborhood wasn't for us.
This one talks about how Mayor Keller is getting "heat."
New Hope has long been known as one of the most gay-friendly towns in the region, a place where rainbow flags flutter in front of boutique shops and the borough council began passing gay-rights resolutions about a decade ago, well before the recent surge nationwide.
This one is from a a web site called American Family Focus on PA Issues. They are applauding the Mayor of New Hope for refusing to marry gay couples in spite of what most legal experts claim are limited risks to him and to the town of New Hope.
Mayor Keller said that as an elected officials it was his duty to uphold the law. The AFA of PA applauds Mayor Keller's decision to uphold the law. Even the Borough Council of State College advised their mayor, who had previously said she would perform same-sex "marriages, not to break the law.
As a side note, I don't think Mayor Keller is actually taking sides on the issue, or that he's in any way associated with American Family Focus on PA Issues. As far as I know, and from what I've read, Mayor Keller supports gay marriage. He just isn't willing to take the legal risks that may or may not be involved with marrying gay couples illegally. But I don't think he gets points for just being for gay marriage, not as a community leader, an elected official, and someone the rest of us all look to for guidance and support. The bright, outspoken woman running against Keller this fall claims she will marry gay couples in spite of any risks involved.
2004 Marriage License Legal in NM
Unlike New Hope, PA, where I live, there have been interesting steps taken this week with regard to same sex marriage. Unlike New Hope, where the mayor of a large LGBT population has decided not to marry gay couples because he's unwilling to take the legal risks involved and is more focused on what may or may not happen if he does, the Attorney Gen. in New Mexico claims that same sex marriage licenses issued in 2004 will remain valid and legal for now.The term he used was "presumptively valid."
King delivered the non-binding advice in a letter to the current Sandoval County clerk, who found that some of the 2004 licenses recorded in the clerk's office were labeled as void or invalid.
King said a county clerk is responsible for issuing marriage licenses but "New Mexico law plainly does not provide county clerks with the rights to invalidate marriages."
There's always a loophole.
Holly Golightly's Story; Cory Booker Gay Rumors
Holly Golightly's Story
This article about the creation of Holly Golightly in Truman Capote's novella, Breakfast at Tiffany's, has several interesting points. One of which deals with her personality and how she thinks about men.
In her disregard for the conventions of polite society and her sexual adventurousness, Holly is something of an avatar of the liberated woman of the Sixties and Seventies, although she probably wouldn't have approved of hippie sartorial practices, nor would she have likely appreciated the more strident male-bashing aspects of the radical wing of the feminist movement.
Truman Capote was a gay man, but not an openly gay man in the sense that he worried about equality and coming out. In his day the word gay meant happy and he was considered a homosexual, among other pejoratives. When he wrote the character of Holly Golightly it most likely came from many of his own personal experiences, because in his time, just like now, the world was owned by straight men.
I found this interesting, too.
One of the strongest endorsements of the novella came from Norman Mailer, normally the most competitive and certainly the most macho of all of Capote's contemporaries, who wrote: "Truman Capote I do not know well, but I like him.
"He is as tart as a grand aunt, but in his way he is a ballsy little guy, and he is the most perfect writer of my generation, he writes the best sentences word for word, rhythm upon rhythm. I would not have changed two words of Breakfast at Tiffany's, which will become a small classic." (Indeed, perfectionist that he was, Capote might well have placed a semicolon after the word "generation". Capote was a master of that particular punctuation mark.)
On the surface that sounds like a compliment, but some gay men would take offense to the grand aunt reference. I know I do. As flamboyant as Capote was, he was still a man. A good deal of his career, however, was spawned as a result of his being so flamboyant, and I'm sure he knew that. Gay men have always done whatever they have to do to survive, and in some cases, if that means acting the part of a pet poodle they are not above that. I understand that, I don't fault them for that, and I admire them for doing what they had to do to survive. I can tell you one thing for certain, if the character of Holly Golightly had been written as a gay man, the book would never have been published, Mailer would never have praised it the way he did in the quote above, and I probably wouldn't even be writing this blog post about it.
I could ramble on with this topic for days. But the point I'm trying to make here is that when I parodied Breakfast at Tiffany's the way I did with gay characters in The Virgin Billionaire, I was making my own statement, not trying to become the next Truman Capote. By writing the VB as an erotic romance only took that parody to another level because that's also something Capote never would have been allowed to do during his time…books about gay men AND sex were hidden in the mattress. And there weren't that many around in the first place. Gay men had nothing with which to identify in books or in films during Capote's time…or any form of mainstream entertainment. So they wound up identifying with characters like Holly Golightly for lack of anything better. And Capote did do a great job of creating her, but I'll always wonder that if he'd lived in a different time and place if he would have made her a gay man instead.
You won't see that mentioned in the article I've linked to. I doubt the author, Jay McInerney, even thinks along those lines. And why should he? He never had to think that way.
I think this next article to which I'm linking is important for a variety of reasons. Cory Booker is a talented young politician I've been watching for a while now. He's the mayor of Newark, NJ, and the things he's done in that city to turn things around have been wonderful. I was born in Newark, NJ, and as a young child my family moved away because the city started to decay. And I never thought I would see such a huge rebound in my lifetime. No one can dispute this.
This fall Cory Booker is running for a seat in the senate, and another senate candidate, Steve Lonegan, has been throwing those proverbial darts in Booker's direction. And the way he's been doing this is not only shocking, it's about as sickening as it gets with regard to what he thinks of gay men in general.
"It's kind of weird. As a guy, I personally like being a guy. I don't know if you saw the stories last year. They've been out for quite a bit about how he likes to go out at three o'clock in the morning for a manicure and a pedicure," Lonegan, the conservative former mayor of Bogota, N.J., told Newsmax.
This comment is an indirect result of the fact that Booker does not comment on his private life or his sexual orientation at all. Booker made this statement last week.
"Because how unfair is it to a young lady to put them in the spotlight if they haven't signed up for that yet?" he said. "And people who think I'm gay, some part of me thinks it's wonderful. Because I want to challenge people on their homophobia. I love seeing on Twitter when someone says I'm gay, and I say, 'So what does it matter if I am? So be it. I hope you are not voting for me because you are making the presumption that I'm straight.'"
I understand what Booker is stating, and I don't disagree with it…if Booker is NOT actually gay. I get the way the political machine works, too. But if he is gay, and he's not disclosing that now, he's really only adding to the shame other gay men have been experiencing all their lives, and promoting the concept that being gay does make a difference. I don't like that. Openly gay men nowadays don't like that. And we are tired of that brand of thinking. Mayor Koch of New York did that sort of thing all his life, and I would like to see that brand of thinking die with Koch's generation so that future generations of gay men don't have to worry about that "young lady" in the spotlight, and all they do have to worry about is that "young man" in the spotlight.
This actually even gets more complicated in this article, where Booker talks about how he once hated gays.
He added: "Allow me to be more direct, escaping the euphemisms of my past — I hated gays. The disgust and latent hostility I felt toward gays were subcategories of hatred, plain and simple."
Booker's self-cleansing column seems to dispute rumors that he is a closeted homosexual. Is it possible for a man to be virulently homophobic and still be gay? One published study suggests that it is within the realm of possibility.
If I were Booker, I would say something one way or the other and address the issue openly. I will never forget the day I came home from work to a news conference on TV where Gov. McGreevey of NJ said, "I am a gay American." It was as entertaining as it was pathetic. I had seen McGreevey in person once in Lambertville, NJ, up close, during a parade. I knew he was gay the moment I looked into his eyes. And this was long before his disclosure. When he did finally decide to come out, blogs all over the web branded him Governor "McCreepy." And I would hate to see Cory Booker turn into Senator Creeper.
Photo here


text:
Scholars of the Week: Ariel Forcey, Sheyanne Burandt
Scholars of the Week for Seymour High School
Scholars of the Week: Ariel Forcey, Sheyanne Burandt Scholars of the Week for Seymour High School Check out this story on greenbaypressgazette.com: http://gbpg.net/1bF1ha2
Press-Gazette Media Published 2:47 p.m. CT March 28, 2015 | Updated 3:51 p.m. CT March 28, 2015
Ariel Forcey and Sheyanne Burandt of Seymour High School(Photo: Submitted)
Seymour High School's Ariel Forcey, daughter of John and Dawn Forcey, is dedicated to her education, community and her future goals. She has earned a 3.88 grade point average while taking advanced, college credit and AP courses.
She enjoys other languages and cultures and has taken Spanish and Japanese while in high school. She is a member of Student Association for Learning Spanish Appreciation (SALSA), Theater Stage Guild and FBLA. Ariel works hard in school and seeks out new challenges.
She has volunteered in the community ringing bells through Salvation Army and at the local library where she helps plan activities and games for kids and parents as part of the summer reading program.
She plans to attend University of Wisconsin-Green Bay and pursue a degree in math.
Sheyanne Burandt, daughter of David and Kim Burandt, is a motivated and hard-working student at Seymour High School. She has earned a 3.9 grade point average while taking advanced and college credit courses. She is a positive leader in the school and in the community.
She is in SALSA, and has been a STEP Crew leader as well as a junior and senior class officer. She spends time outside of school volunteering with her church on mission trips and at vacation bible school.
She has also helped out others at CHAPS Academy as well. She has won several awards through the National Barrel Horse Association, and was invited to the world finals. Her activities fit well with her future plans of becoming a large animal veterinarian.
She plans pursue this at the University of Wisconsin-Madison.
Read or Share this story: http://gbpg.net/1bF1ha2


text:
Condylostylus basilaris är en tvåvingeart som först beskrevs av Christian Rudolph Wilhelm Wiedemann 1830.  Condylostylus basilaris ingår i släktet Condylostylus och familjen styltflugor. Inga underarter finns listade i Catalogue of Life.

Källor

Styltflugor
basilaris

redpajama_set_name: RedPajamaWikipedia


We know that at RF Blount & Sons that it's our people who will ensure our continued success and development.
That's why we carefully select our staff for their knowledge and experience. We pride ourselves on employing the right people for the job.
So, if you think that you've got what it takes, perhaps you can look forward to the opportunity of building a strong and lasting career within RF Blount & Sons.
Please contact us and provide details of your experience and qualifications. References are welcome.


Beloved Brothers and Sisters of Earth, I AM Emmanuel and I welcome you to this moment.
Question: You said that two people -even close neighbors- would experience different outcomes from the 2012 events, like one will experience ascension and the other one catastrophe. Could you please elaborate on this?
For two individuals to experience the same event they have to share the same portion of the vibratory spectrum. All possible combination of frequencies, including all planes in all universes exist within your consciousness, but are only the vibrations that passes through your awareness are the ones you perceive.
Many of you believe that previous to incarnation you choose the life-events you wish to experience in order to learn certain lesson and grow as individual, but in fact you did not choose the life-events but the vibrations you want to experience. After incarnation is all up to you. It is you, acting on free-will, who creates the events that occurs in your life, and if those events lead you to experience the vibrations you choose to experience as part of your spiritual growth, you have achieved. Then you can move on, otherwise you will have to try again.
So after incarnation you have two ways of succeeding, the first one is to create the right life-events, and the second one is expanding your awareness. It is up to you to choose the way with which you the greatest affinity and therefore the greatest chance of success.
The frequencies of all the universes can be seen as energetic lines or strings.
Like the strings on the guitar, and the sound-hole is your awareness.
The larger the sound-hole is, the more strings will resonate.
When you expand your awareness the world you perceive expands, allowing more energetic lines through, expanding the segment of the vibratory spectrum accessible to you, hence increasing exponentially the chances of experiencing the group/kind of vibration you came here to experience.
Awareness can be seen as circles, two individual's circles may intersect or not. Two individuals will share the same world only in the area of intersection.


text:
Mathematical Treasures - Frans van Schooten's Exercitationes mathematicae
Frank J. Swetz and Victor J. Katz
This is the title page of Exercitationes mathematicae libri quinque (Five Books of Mathematical Exercises) (1657) by Frans van Schooten (1615-1660). In particular, according to the inscription, this copy was originally owned by Johann Hudde (1628-1704), a student of van Schooten. The five books collected in this work contained a variety of mathematical material, including sections on basic arithmetic and geometry, simple geometric constructions, an attempted reconstruction of a work of Apollonius, constructions of conic sections, and some combinatorial techniques enabling him to find amicable numbers. Van Schooten also included as an appendix the first text on probability, written by Christiaan Huygens (1629-1695), again one of his students. This collection was one of the books read by Isaac Newton while he was a student at Cambridge University and helped to introduce him to modern mathematics.
This is page 167 in the section on geometrical constructions. This particular construction shows how to find the distance across a river.
On p. 223, van Schooten begins his section on reconstruction of the Plane Loci of Apollonius. Interestingly, although van Schooten only knew of the Plane Loci from various Greek references, more recently the actual work was discovered in an Arabic version.
On p. 224, van Schooten shows how, given points A and B, to construct two line segments AG and BG that meet at a given angle.
On page 327, van Schooten demonstrates the use of linkages to construct ellipses.
On p. 533 is the final proposition in Huygens' Treatise on Reckoning in Games of Chance. This particular problem asks to determine the ratio of "chances" in a game where two people play alternately with two dice, on the condition that the first one wins when he throws a 7, while the second one wins if he throws a 6, assuming that the second player throws first. Huygens' solution is that the ratio is 31:30.
At the bottom of p. 533 and on p. 534 are five exercises that conclude Huygens' treatise. For example, in problem 2, Huygens sets up the situation where there are 12 balls in an urn, of which 4 are white and 8 are black. There are three blindfolded players A, B, and C who draw a ball out in turn with the winner being the first one to draw out a white ball. Huygens asks the ratio of the chances of the three players. (As stated, the problem is somewhat ambiguous, but it is probably easiest to assume that if a black ball is drawn, it is put back into the urn.)


text:
» Lady Chatterley's lover
Lady Chatterley's Lover
Tantor Media, Inc., 2011.
26af3a7f-5b0a-ee27-b8ce-9e4bf8811c9b
lady chatterleys lover
lawrence d h
[artist] => D. H. Lawrence
[coverImageUrl] => https://d2snwnmzyr8jue.cloudfront.net/ttm_9781452621050_270.jpeg
[title] => Lady Chatterley's Lover
[duration] => 12h 0m 0s
[name] => D. H. Lawrence
[name] => John Lee
[0] => Fiction
[synopsis] => The last and most famous of D. H. Lawrence's novels, Lady Chatterley's Lover was published in 1928 and banned in England and the United States as pornographic. While sexually tame by today's standards, the book is memorable for better reasons-Lawrence's masterful and lyrical prose, and a vibrant story that takes us bodily into the world of its characters.As the novel opens, Constance Chatterley finds herself trapped in an unfulfilling marriage to a rich aristocrat whose war wounds have left him paralyzed and impotent. After a brief but unsatisfying affair with a playwright, Lady Chatterley enjoys an extremely passionate relationship with the gamekeeper on the family estate, Oliver Mellors. As Lady Chatterley falls in love and conceives a child with Mellors, she moves from the heartless, bloodless world of the intelligentsia and aristocracy into a vital and profound connection rooted in sexual fulfillment.Through this novel, Lawrence attempted to revive in the human consciousness an awareness of savage sensuality, a sensuality with the power to free men and women from the enslaving sterility of modern technology and intellectualism. Perhaps even more relevant today than when it first appeared, Lady Chatterley's Lover is a triumph of passion and an erotic celebration of life.
[publisher] => Tantor Media, Inc.


A. Physical and chemical vapour deposition techniques, thermal and plasma spraying, electroplating and surface modification by directed energy techniques such as ion, electron and laser beams.
B. Characterization and evaluation of coatings and modified surfaces. Investigation of their tribological behaviour or interactions with the environment.
C. Surface engineering to improve friction performance, wear resistance (e.g., abrasion, erosion, fretting, etc), to provide protection against corrosion phenomena (e.g., in aqueous solutions or at high temperature) and/or ensure thermal protection, diffusion resistance and hydrophobicity.
D. Coatings and surface engineering solutions to improve the operating performance of component surfaces, for example in energy and medical applications, but excluding device aspects.
Articles must go beyond the technical recipe format and gain new understanding and insight based on detailed characterization of coatings and processes. Experimental papers should provide complete information on the process parameters and an appropriate microstructural characterization.